functor AsmProver (S : ASMPROVER_STRUCTS) : ASMPROVER =
struct
open S
     
structure E = ErrorMsg
structure A = Asm

exception AsmProverFail
val error = E.error

val debugFlag = fn () => !Control.doShowAsmPrf
val showFailEvn = false
val showAsmEnv = false
val showInternalResult = true
val adjustdebugFlag = false

val postcondition = ref (SOME A.Ptrue)
val plist : A.pprf list ref  = ref []
 
fun debugPrint str = if debugFlag () then print str else ()
fun adjustDebugPrint str = if adjustdebugFlag then print str else ()             
fun printC (myprint, str) = myprint (str^"   ")

datatype ptrsort 
  = P 
  | N
  | D
  | U

(*----------------------------------Function ret parameter type-----------------*)
fun getFnRetType (f, ginf) = 
    let val tp = A.getFRet(f, ginf)
        val _ = debugPrint (f^" return value type is "^A.etype2str(tp)^"\n")
    in tp
    end

fun getFnParameters f = 
    let val tl = A.getParas(!plist, f)
        fun pp a =
            let val (aptr, tp) = a
                val _ = (debugPrint (A.aptr2str(aptr)^" : "^A.etype2str(tp)^"\n"))
                fun chOff aptr =
                    case aptr
                     of A.Pstk(off, reg) => A.Pstk(off-8, reg)
                      | _ => (debugPrint "Function Parameter Bug...\n" ; raise AsmProverFail)
            in (chOff aptr, tp)
            end
    in List.map pp tl
    end

(*--------------------------------debug info------------------------------------*)
type debuginfo = {fname : string
                , label : string
                , instr : string
                , pos   : string} 

fun getDebugFname (dinfo : debuginfo)= #fname dinfo 
fun getDebugLabel (dinfo : debuginfo) = #label dinfo
fun getDebugInstr (dinfo: debuginfo) = #instr dinfo
fun getDebugPos (dinfo : debuginfo) = #pos dinfo

fun setDebugFname (fname) =
    {fname = fname 
   , label = ""
   , instr = ""
   , pos   = ""} 

fun setDebugLabel (dinfo, label) = 
    {fname = getDebugFname dinfo
   , label = label
   , instr = getDebugInstr dinfo
   , pos   = getDebugPos dinfo}

fun setDebugInstr (dinfo, instr) =
    {fname = getDebugFname dinfo 
   , label = getDebugLabel dinfo
   , instr = A.toString instr
   , pos   = getDebugPos dinfo}

fun setDebugPos (dinfo : debuginfo, pos) =  
    {fname = getDebugFname dinfo 
   , label = getDebugLabel dinfo
   , instr = getDebugInstr dinfo
   , pos   = pos}

fun getDebugInfoStr (dinfo : debuginfo) =
    let val f = "Function Name : \t"^getDebugFname(dinfo)^"\n"
        val l = "Label Name    : \t"^getDebugLabel(dinfo)^"\n"
        val i = "Instruction   : "^getDebugInstr(dinfo)^"\n"
        val p = "Error         : \t"^getDebugPos(dinfo)^"\n"
    in f^l^i^p
    end

(*----------------------------aptr utils-----------------------------------------*)

fun isAptrReg (aptr) =
    case aptr
     of A.Preg _ => true
      | A.Pstk(off,reg) =>
        (case reg 
          of A.Ebp => false
           | A.Esp => false
           | _ => true)
      | A.Pmem(off,aptr1,pexp) =>
        isAptrReg (aptr1)        
      | _ => false

(*aptr in pexp?*)
fun inPexp (aptr, testpexp) =
  case testpexp
   of A.Pvar(aptr1) => (inAptr (aptr, aptr1))
    | A.PintNum(i) => false
    | A.Pplus(pexp1, pexp2) => (inPexp (aptr, pexp1) orelse inPexp (aptr, pexp2))
    | A.Pminus(pexp1, pexp2)=> (inPexp (aptr, pexp1) orelse inPexp (aptr, pexp2))
    | A.Ptimes(pexp1, pexp2)=> (inPexp (aptr, pexp1) orelse inPexp (aptr, pexp2))

(*aptr in another aptr?*)
and inAptr (aptr, testaptr) =
    if aptr = testaptr
    then true
    else case testaptr
          of A.Preg(reg) => false
           | A.Pstk(off,reg) => (aptr = A.Preg(reg))
           | A.Pmem(off,aptr1,pexp)=> 
             (inAptr (aptr, aptr1) orelse inPexp (aptr, pexp))
           | A.Pgmem(l) => false
           | A.Pid(str) => false

(*aptr compare*)
fun aptr_compare (aptr1, aptr2) =
    case (aptr1, aptr2)
     of  (A.Preg r1, A.Preg r2) => 
         let val _ = debugPrint ""
         in
             if r1 = r2 
             then EQUAL
             else LESS
         end
    | (A.Pstk (off1, r1), A.Pstk (off2, r2)) =>
      if off1 = off2 andalso r1 = r2
      then EQUAL
      else LESS
    | (A.Pmem(o1, a1, p1), A.Pmem(o2, a2, p2)) =>
      if o1 = o2 andalso p1 = p2 andalso aptr_compare(a1, a2) = EQUAL
      then EQUAL
      else LESS
    | (A.Pgmem l1, A.Pgmem l2) =>
      if l1 = l2
      then EQUAL
      else LESS
    | (A.Pid s1, A.Pid s2) =>
      if s1 = s2 
      then EQUAL
      else LESS
    | (_, _) => LESS

(*-------------------------------------Pi N D U-------------------------------------*)  
(*set*)         
structure NDSet = BinarySetFn(struct type ord_key=A.aptr val compare=aptr_compare end)
                  
fun set_compare (s1, s2) =
    let val size1 = NDSet.numItems s1
        val size2 = NDSet.numItems s2
    in if (size1 <> size2)
       then LESS
       else let val l1 = NDSet.listItems s1
                val l2 = NDSet.listItems s2
                fun inList (aptr, list) =
                    case list
                     of [] => 0
                      | a::l => if a = aptr then 1 else inList (aptr, l)
                val fl = List.map (fn aptr => inList (aptr, l2)) l1
                val n = List.foldl (op +) 0 fl
            in if (n = size1) then EQUAL else LESS
            end
    end

(*set set*)
structure PiSet = BinarySetFn(struct type ord_key=NDSet.set val compare=set_compare end)

(*empty set*)
val emp_pi = PiSet.empty
val emp_n  = NDSet.empty
val emp_d  = NDSet.empty
val emp_u  = PiSet.empty

(* equality test *)
fun isEqPi (pi1, pi2) = PiSet.equal (pi1, pi2)

fun isEqN  (s1, s2)   =
    let val size1 = NDSet.numItems s1
        val size2 = NDSet.numItems s2
    in if (size1 <> size2)
       then false
       else let val l1 = NDSet.listItems s1
                val l2 = NDSet.listItems s2
                fun inList (aptr, list) =
                    case list
                     of [] => 0
                      | a::l => if a = aptr then 1 else inList (aptr, l)
                val fl = List.map (fn aptr => inList (aptr, l2)) l1
                val n = List.foldl (op +) 0 fl
            in  if (n = size1)
                then true
                else false
            end
    end

fun isEqD  (d1, d2)   = isEqN (d1, d2)
fun isEqU  (u1, u2)   = PiSet.equal (u1, u2)
                        
(* emxptiness test *)
fun isEmptyPi pi = PiSet.isEmpty pi
fun isEmptyN  n  = NDSet.isEmpty n
fun isEmptyD  d  = NDSet.isEmpty d
fun isEmptyU  u  = PiSet.isEmpty u

(*set list convertion*)
fun toSet aptrList = NDSet.addList(NDSet.empty, aptrList)
fun toSetSet aptrlistlist = PiSet.addList(PiSet.empty, List.map toSet aptrlistlist)
                            
fun toList set = NDSet.listItems set
fun toListlist setset = List.map toList (PiSet.listItems setset)

(*test correctness of Pi N D U set *)
fun isPiNDUCorrect (pi, n, d, u) = 
    if isEmptyPi pi andalso isEmptyN n andalso isEmptyD d andalso isEmptyU u
    then true
    else let val ndsize = NDSet.numItems n + NDSet.numItems d
             val pisize = List.foldl op + 0 (List.map (NDSet.numItems) (PiSet.listItems pi))
             val usize  = List.foldl op + 0 (List.map (NDSet.numItems) (PiSet.listItems u))
             val ndlist = List.concat [(toList n),(toList d)]
             val pilist = List.concat (toListlist pi)
             val ulist  = List.concat (toListlist u)
             val newlist = List.concat [ndlist, pilist, ulist]
             val newsize = NDSet.numItems (toSet newlist)
         in (ndsize + pisize + usize) = newsize
         end
(*set setset output*)    

fun printSet (myprint, set) = 
    (myprint "{"; List.app (fn str => printC (myprint, str))  (List.map (A.aptr2str) (NDSet.listItems set)); myprint "} \n")

fun printSetset (myprint, setset) = 
    (myprint "{\n"; List.app (fn set => printSet (myprint, set)) (PiSet.listItems setset); myprint "}")

fun outputPiNDU (PiSet, NSet, DSet, USet) flag =
    let val myPrint = if not flag then debugPrint else print
        val _ = (myPrint ("PiSet: "); printSetset (myPrint, PiSet); myPrint "\n" )                               
        val _ = (myPrint ("N Set: "); printSet (myPrint, NSet); myPrint "\n")
        val _ = (myPrint ("D Set: "); printSet (myPrint, DSet); myPrint "\n")   
        val _ = (myPrint ("U Set: "); printSetset (myPrint, USet); myPrint "\n" )
    in ()
    end

(*--------------------Pi Set and alias-----------------------------*)
(* setlower transform *)
(* {se} => se, and no execption should be raised... *)
fun set2elem setset = 
    let val set = if isEmptyPi setset
                  then [emp_n]
                  else PiSet.listItems setset
    in if List.null set
       then emp_n
       else List.hd set
    end
    
(* p {{p, q}, ...} => {{p, q}} *)
and getPtrSet (aptr, pi) =
    let val _ = debugPrint ""
        fun get l =
            case l
             of [] => emp_n
              | x :: xs =>
                if isPtrInN (aptr, x)
                then x
                else get xs
    in  PiSet.singleton (get (PiSet.listItems pi))
    end

(* p {{p, q}, ...} => {p, q} *)
and getPtrSetItem (aptr, pi) =
    let val setOfPtr = NDSet.singleton aptr
        val setset = getPtrSet (aptr, pi)
    in set2elem setset
    end

(*get an alias*)
and getAnotherPtrSameSetPi (aptr, pi) =
    let val setOfPtr = NDSet.singleton aptr
        val set = getPtrSetItem (aptr, pi)
        val l = toList set
        fun find (aptr0, list) =
            case list
             of [] => aptr0
              | x :: xs => 
                if x = aptr0 orelse (inAptr (aptr0, x)) (*edited 8-14 16:13*)
                then find (aptr0, xs)
                else x
    in find (aptr, l)
    end

(*---------------------Membership-------------------*)
(*membership of Pi*)
and isPtrInPi (aptr, pi) = 
    let val _ = debugPrint ""
        fun check l =
            case l
             of [] => false
              | x :: xs => 
                if isPtrInN (aptr, x)
                then true
                else check xs
    in  check (PiSet.listItems pi)
    end

and is2PtrInPiSameSet (aptr1, aptr2, pi) = 
    if isEmptyPi pi
    then false
    else if isPtrInPi(aptr1, pi) andalso isPtrInPi(aptr2, pi)
         then let val setset1 = getPtrSet (aptr1, pi)
                  val setset2 = getPtrSet (aptr2, pi)
              in if isEqPi(setset1, setset2)
                 then true
                 else false
              end
         else false       
    
and isPtrInSingletonPi (aptr, pi) =
    let val setOfPtr = NDSet.singleton aptr
        val filterPi = getPtrSet (aptr, pi)
    in if isEmptyPi filterPi
       then false
       else if isEqPi (PiSet.singleton setOfPtr, filterPi)
            then true
            else false
    end

(*membership of U*)
and isPtrInU (aptr, u) = 
    let val _ = debugPrint ""
        fun check l =
            case l
             of [] => false
              | x :: xs => 
                if isPtrInN (aptr, x)
                then true
                else check xs
    in  check (PiSet.listItems u)
    end

and is2PtrInUSameSet (aptr1, aptr2, u) = 
    if isEmptyU u
    then false
    else if isPtrInU(aptr1, u) andalso isPtrInU(aptr2, u)
         then let val setset1 = getPtrSet (aptr1, u)
                  val setset2 = getPtrSet (aptr2, u)
              in if isEqU (setset1, setset2)
                 then (debugPrint "true branch\n"; true)
                 else (debugPrint "false branch\n"; false)
              end
         else false       
    
and isPtrInSingletonU (aptr, u) =
    let val setOfPtr = NDSet.singleton aptr
        val filterU = getPtrSet (aptr, u)
    in if isEmptyU filterU
       then false
       else if isEqU (PiSet.singleton setOfPtr, filterU)
            then true
            else false
    end

(*membership of N D*)
and isPtrInN (aptr, n) =
      let val _ = debugPrint ""
          fun check l =
              case l
               of [] => false
                | x :: xs => 
                  if x = aptr
                  then true
                  else (check xs)
      in  check (NDSet.listItems n)
      end
      
  and isPtrInD (aptr, d) =
      let val _ = debugPrint ""
          fun check l =
              case l
               of [] => false
                | x :: xs => 
                  if x = aptr
                  then true
                  else (check xs)
      in  check (NDSet.listItems d)
      end
fun isPtrInN2 (aptr, n) = NDSet.member(n, aptr)
fun isPtrInD2 (aptr, d) = NDSet.member(d, aptr)
fun isPtrInND (aptr, n, d) = 
    if isPtrInN(aptr, n) orelse isPtrInD(aptr, d)
    then true
    else false

(*ptr sort ---P N D U*)
fun getPtrSort (aptr, pndu) =
    let val (pi, n, d, u) = pndu
    in if not (isPiNDUCorrect (pi, n, d, u))
       then (outputPiNDU (pi, n, d, u) true ; raise Fail "ptr set bug") (*fail*)
       else if isPtrInPi (aptr, pi)
            then P
            else if isPtrInN (aptr, n)
                 then N
                 else if isPtrInD (aptr, d)
                      then D
                      else U
    end                   

(*not leaking*)
fun not_leaking (aptr, pi) =
    if isPtrInSingletonPi (aptr, pi) 
    then false
    else true       
                         
(* -------------------add elem------------------- *)
(*Pi*)
(* p + {...} => {{p}, ...} *)
and addSingletonPi (aptr, pi) =
    let val setOfPtr = NDSet.singleton aptr
    in  PiSet.add(pi, setOfPtr)
    end
(* p + {{q,...}, ...} => {{p, q,...}, ...} *)
and addPtrPi (aptr, aim, pi) = 
    let val set = set2elem (getPtrSet (aim, pi))  (* {q, ...} *)
        val set2 = NDSet.add (set, aptr)        (* {p, q, ...}*)
        val newPi = deleteSetPi (set, pi)     (* {...} *)
    in PiSet.add (newPi, set2)
    end

and addSetPi (set, pi) = PiSet.add (pi, set)
(*N D*)
and addPtrN (aptr, n) = 
    if isPtrInN (aptr, n)
    then n
    else NDSet.add(n, aptr)
and addPtrD (aptr, d) = 
    if isPtrInN (aptr, d)
    then d 
    else NDSet.add(d, aptr)
(*U*)
and addSingletonU (aptr, u) = addSingletonPi (aptr, u)
and addPtrU (aptr,aim, u) = addPtrPi( aptr, aim ,u)

(* -------------------delete elem------------------- *)

and deleteSetInPi (set, pi) = 
    let fun del inlist =
            case inlist
             of [] => []
              | x :: xs =>
                if isEqN (set, x)
                then (del xs)
                else (toList x) :: (del xs)
        val newlistlist = del (PiSet.listItems pi)
    in  toSetSet newlistlist
    end

and deletePtrInSet (aptr, set) =
    let fun del inlist =
            case inlist
             of [] => []
              | x :: xs =>
                if x = aptr 
                then xs
                else x::(del xs)
        val newalist = del (toList set)
    in toSet newalist
    end
(* no exeption should be raised... *)
(* {a, b} {{a, b},...} => {...} *)
and deleteSetPi (set, pi) = deleteSetInPi(set, pi)
         

and deletePtrSetPi (aptr, pi) =
    let val filter_pi = set2elem (getPtrSet (aptr, pi))
    in deleteSetPi (filter_pi, pi)
    end
(* {{p, q}, {s, t, r}} => {{q}, {s, t, r}}*)
(* one point to note: {{p}, {s, t, r}} => {{s, t, r}}, but not {{}, {s, t, r}} *)

and deleteRegPtrND (set) =
    let val l = toList set
        fun del l =
            case l
             of [] => []
              | x::xs =>
                (case x
                  of A.Preg _ => del xs
                   |_ =>  x::(del xs)
                )
    in toSet (del l)
    end

and deleteRegPtrPi (pi) =
    let val setlist = PiSet.listItems pi
    in PiSet.addList(emp_pi, List.map deleteRegPtrND setlist)
    end
    
and deletePtrPi (aptr, pi) =
      let val filterPi = set2elem (getPtrSet (aptr, pi))
          val npi = if isPtrInSingletonPi (aptr, pi)
                    then  deleteSetPi (filterPi, pi)
                    else if NDSet.isEmpty filterPi
                         then raise Fail "bug"
                         else let val tpi = deleteSetPi (filterPi, pi)
                                  val _ = printSetset (debugPrint, pi)
                                  val _ = printSet (debugPrint, filterPi)
                                  val _ = printSetset (debugPrint, tpi)
                                  val subset = filterPi
                                  val tset = deletePtrInSet (aptr, subset)
                                  val fpi = PiSet.add (tpi, tset)
                                  val _ = printSet (debugPrint, tset)
                                  val _ = printSetset (debugPrint, fpi)
                              in  fpi
                              end                                                  
      in npi
      end

fun deletePtrN (aptr, n) = deletePtrInSet (aptr, n) 
fun deletePtrD (aptr, d) = deletePtrInSet (aptr, d)

fun deleteSetU (set, u)  = deleteSetPi (set, u)
fun deletePtrU (aptr, u) = deletePtrPi (aptr, u)

(*-----------------------------------ptr in PiP?------------------------------------*)

fun isPtrInAptr (aptr, aimaptr) = if aptr = aimaptr then true else false
     
fun isPtrInPexp (aptr, pexp) = 
    case pexp
     of A.Pvar(aptr1) =>isPtrInAptr(aptr, aptr1)
      | _ => false
 

fun isPtrInPiP (aptr, pip) = 
    case pip 
     of A.Pand(p1, p2) => 
        if isPtrInPiP (aptr, p1) orelse isPtrInPiP (aptr, p2)
        then true
        else false
      | A.Peq(pe1, pe2)=>
        if isPtrInPexp (aptr, pe1) orelse isPtrInPexp (aptr, pe2)
        then true
        else false
      | _ => false

(*----------------------------------adjust Pi N D U------------------------------------*)
                           
and adjustAptrSubI (aptr, i, aimaptr) =
    let val _ = adjustDebugPrint "Adjust Aptr \n"   
        val adp = fn aim => adjustPexpSubI (aptr, i, aim)
        val ada = fn aim => adjustAptrSubI (aptr, i, aim)
    in case aimaptr
        of A.Preg(reg) => A.Preg(reg)
         | A.Pstk(off,reg) => 
           if (A.Preg(reg) = aptr) 
           then A.Pstk(off-i,reg)
           else A.Pstk(off,reg)
         | A.Pmem(off,aptr1,pexp) => 
           if (aptr1 = aptr) 
           then A.Pmem(off-i,aptr1, adp pexp)
           else A.Pmem(off,(ada aptr1), adp pexp)
         | A.Pgmem(l) => A.Pgmem(l)
         | A.Pid(str) => A.Pid(str)
    end

and adjustAptrListSubI (aptr, i, list) = 
    List.map (fn aim => adjustAptrSubI (aptr, i, aim)) list

and adjustPexpSubI (aptr, i, pexp) = 
    let val _ = adjustDebugPrint "Adjust pexp \n"
        val adp = fn aim => adjustPexpSubI (aptr, i, aim)
        val ada = fn aim => adjustAptrSubI (aptr, i, aim)
    in case pexp
        of A.Pvar(aptr1) => A.Pvar(ada aptr1)
         | A.PintNum(i) => A.PintNum(i)
         | A.Pplus(pexp1, pexp2) => A.Pplus(adp pexp1 , adp pexp2)
         | A.Pminus(pexp1, pexp2)=> A.Pminus(adp pexp1 , adp pexp2)
         | A.Ptimes(pexp1, pexp2)=> A.Ptimes(adp pexp1 , adp pexp2)
    end

and adjustPpropSubI (aptr, i, pprop) =
    let val _ = adjustDebugPrint "Adjust Pprop  "
        val adp = fn aim => adjustPexpSubI (aptr, i, aim)
        val ada = fn aim => adjustAptrSubI (aptr, i, aim)
        val adr = fn prp => adjustPpropSubI (aptr, i, prp)
        val adl = fn l   => adjustAptrListSubI (aptr, i, l)
    in case pprop
        of A.Ptrue        => A.Ptrue
         | A.Pnot(p)      => A.Pnot(adr p)
         | A.Pand(p1, p2) => A.Pand(adr p1, adr p2)
         | A.Por(p1, p2)  => A.Por(adr p1, adr p2)
         | A.Pge(pe1, pe2)=> A.Pge(adp pe1, adp pe2)
         | A.Pgt(pe1, pe2)=> A.Pgt(adp pe1, adp pe2)
         | A.Plt(pe1, pe2)=> A.Plt(adp pe1, adp pe2)
         | A.Ple(pe1, pe2)=> A.Ple(adp pe1, adp pe2)
         | A.Peq(pe1, pe2)=> A.Peq(adp pe1, adp pe2)
         | A.Pne(pe1, pe2)=> A.Pne(adp pe1, adp pe2)
         | A.Pforall((str, tp), p) => A.Pforall((str, tp), adr p)
         | A.Pex((str, tp), p)     => A.Pex((str, tp), adr p)
         | A.Pi(aptrlistlist) => A.Pi(List.map adl aptrlistlist)
         | A.N(aptrlist)      => A.N(adl aptrlist)
         | A.D(aptrlist)      => A.D(adl aptrlist)
         | A.Ptree(pe) => A.Ptree(adp pe)
         | A.Plist(pe) => A.Plist(adp pe)
         | A.Ppred(str,p) => A.Ppred(str, adr p)
    end
    
fun adjustNDSubI (aptr, i, set) = 
    if (isEmptyN set)
    then set
    else let val l = toList set
             val set2 = toSet (adjustAptrListSubI (aptr, i, l))
         in set2
         end
        
fun adjustPiSubI (aptr, i, pi) =
    if (isEmptyPi pi)
    then pi
    else let val ll = toListlist pi
             val ll2 = List.map (fn l => adjustAptrListSubI (aptr, i,l)) ll
             val pi2 = toSetSet ll2
         in pi2
         end   

fun adjustUSubI (aptr, i, u) = 
    if (isEmptyU u)
    then u
    else let val ll = toListlist u
             val ll2 = List.map (fn l => adjustAptrListSubI (aptr, i,l)) ll
             val u2 = toSetSet ll2
         in u2
         end

(*----------------------------------delete aptr base-------------------------*)
fun isAptrBase (aptr, aimaptr) = 
    let val _ = adjustDebugPrint "is aptr base \n"  
    in if aptr = aimaptr
       then true
       else case aimaptr
             of A.Preg(reg) => false
              | A.Pstk(off,reg) => 
                if (aptr = A.Preg(reg))
                then true
                else false
              | A.Pmem(off,aptr1,pexp) =>
                if isAptrBase (aptr, aptr1) (*aptr = aptr1*)(*8.22XXXXX*)
                then true
                else false
              | A.Pgmem(l) => false
              | A.Pid(str) => false
    end
    
fun deleteNDBase (aptr, set) = 
    let val _ = adjustDebugPrint "delete  N or D base ...\n"
    in if (isEmptyN set)
       then set
       else let val l = toList set
            in case l
                of [] => set
                 | aimaptr::ll =>
                   let val set2 = toSet ll
                       val set3 = deleteNDBase(aptr, set2)
                   in if isAptrBase (aptr, aimaptr)
                      then set3
                      else toSet (aimaptr::(toList set3))
                   end
            end
    end

fun deleteUBase (aptr, u) =
    let val _ = adjustDebugPrint "delete U base ...\n"
    in if (isEmptyU u)
       then u
       else let val ll = toListlist u
                val deleteSetBase = 
                 fn l => let val set = toSet l
                             val set2 = deleteNDBase (aptr, set)
                         in toList set2
                         end             
                fun delNullSet listlist =
                    case listlist
                     of [] => []
                      | [] :: xs => delNullSet xs
                      | x :: xs => x :: (delNullSet xs)
                val ll2 = List.map (deleteSetBase) ll
                val u2 = toSetSet (delNullSet ll2)
            in u2
            end  
    end

fun deleteNDBaseReg n =
    let val n1 = deleteNDBase (A.Preg(A.Eax), n)
        val n2 = deleteNDBase (A.Preg(A.Ebx), n1)
        val n3 = deleteNDBase (A.Preg(A.Ecx), n2)
        val n4 = deleteNDBase (A.Preg(A.Edx), n3)
        val n5 = deleteNDBase (A.Preg(A.Esi), n4)
        val n6 = deleteNDBase (A.Preg(A.Edi), n5)
    in n6
    end

fun deleteUBaseReg u =
    let val u1 = deleteUBase (A.Preg(A.Eax), u)
        val u2 = deleteUBase (A.Preg(A.Ebx), u1)
        val u3 = deleteUBase (A.Preg(A.Ecx), u2)
        val u4 = deleteUBase (A.Preg(A.Edx), u3)
        val u5 = deleteUBase (A.Preg(A.Esi), u4)
        val u6 = deleteUBase (A.Preg(A.Edi), u5)
    in u6
    end

(*----------------------------------change aptr to aptr'----------------------*)
fun adjustAptrBase (oldaptr, newaptr, aimaptr) = 
    let val _ = adjustDebugPrint "Adjust aptr from old to new \n"  
        val _ = adjustDebugPrint ("@oldaptr, newaptr aimaptr :"^A.aptr2str(oldaptr)^" "^A.aptr2str(newaptr)^" "^A.aptr2str(aimaptr)^"\n")
        val adp = fn p => adjustPexpBase (oldaptr, newaptr, p)
        val ada = fn a => adjustAptrBase (oldaptr, newaptr, a)
    in case aimaptr
        of A.Preg(reg) => A.Preg(reg)
         | A.Pstk(off,reg) => 
           if (oldaptr = A.Preg(reg))
              then (case newaptr 
                    of A.Preg(reg2) =>  A.Pstk(off, reg2)
                     | _ =>  A.Pmem(off, newaptr, A.PintNum(0)))
              else A.Pstk(off, reg)
         | A.Pmem(off,aptr1,pexp) =>
           if oldaptr = aptr1
           then A.Pmem(off, newaptr, adp pexp)
           else A.Pmem(off, ada aptr1, adp pexp)
         | A.Pgmem(l) => A.Pgmem(l)
         | A.Pid(str) => A.Pid(str)
    end

and adjustAptrListBase (oldaptr, newaptr, list) = 
    List.map (fn a => adjustAptrBase (oldaptr, newaptr, a)) list

and adjustPexpBase (oldaptr, newaptr, pexp) = 
    let val _ = adjustDebugPrint "Adjust pexp from old to new \n"
        val adp = fn p => adjustPexpBase (oldaptr, newaptr, p)
        val ada = fn a => adjustAptrBase (oldaptr, newaptr, a)
    in case pexp
        of A.Pvar(aptr1) => A.Pvar(ada aptr1)
         | A.PintNum(i) => A.PintNum(i)
         | A.Pplus(pexp1, pexp2) => A.Pplus(adp pexp1, adp pexp2)
         | A.Pminus(pexp1, pexp2)=> A.Pminus(adp pexp1, adp pexp2)
         | A.Ptimes(pexp1, pexp2)=> A.Ptimes(adp pexp1, adp pexp2)
    end

and adjustPpropBase (oldaptr, newaptr, pprop) =
    let val _ = adjustDebugPrint "Adjust Pprop from old to new \n"
        val adpe = fn p => adjustPexpBase (oldaptr, newaptr, p)
        val adpr = fn r => adjustPpropBase (oldaptr, newaptr, r)
        val adli = fn l => adjustAptrListBase (oldaptr, newaptr, l)
    in case pprop
        of A.Ptrue        => A.Ptrue
         | A.Pnot(p)      => A.Pnot(adpr p)
         | A.Pand(p1, p2) => A.Pand(adpr p1 ,adpr p2)
         | A.Por(p1, p2)  => A.Por(adpr p1, adpr p2)
         | A.Pge(pe1, pe2)=> A.Pge(adpe pe1, adpe pe2)
         | A.Pgt(pe1, pe2)=> A.Pgt(adpe pe1, adpe pe2)
         | A.Plt(pe1, pe2)=> A.Plt(adpe pe1, adpe pe2)
         | A.Ple(pe1, pe2)=> A.Ple(adpe pe1, adpe pe2)
         | A.Peq(pe1, pe2)=> A.Peq(adpe pe1, adpe pe2)
         | A.Pne(pe1, pe2)=> A.Pne(adpe pe1, adpe pe2)
         | A.Pforall((str, tp), p) => A.Pforall((str, tp), adpr p)
         | A.Pex((str, tp), p)     => A.Pex((str, tp), adpr p)
         | A.Pi(aptrlistlist)      => A.Pi(List.map (adli) aptrlistlist)
         | A.N(aptrlist)           => A.N(adli aptrlist)
         | A.D(aptrlist)  => A.D(adli aptrlist)
         | A.Ptree(pe)    => A.Ptree(adpe pe)
         | A.Plist(pe)    => A.Plist(adpe pe)
         | A.Ppred(str,p) => A.Ppred(str, adpr p)
    end
    
fun adjustNDBase (oldaptr, newaptr, set) = 
    let val _ = adjustDebugPrint "adjust N or D base ...\n"
    in if (isEmptyN set)
       then set
       else let val l = toList set
                val set2 = toSet (adjustAptrListBase (oldaptr, newaptr, l))
            in set2
            end
    end
        
fun adjustPiBase (oldaptr, newaptr, pi) =
    let val _ = adjustDebugPrint "adjust Pi base ...\n"
    in if (isEmptyPi pi)
       then pi
       else let val ll = toListlist pi
                val ll2 = List.map (fn l => adjustAptrListBase (oldaptr, newaptr, l)) ll
                val pi2 = toSetSet ll2
            in pi2
            end  
    end

fun adjustUBase (oldaptr, newaptr, u) =
    let val _ = adjustDebugPrint "adjust U base ...\n"
    in if (isEmptyU u)
       then u
       else let val ll = toListlist u
                val ll2 = List.map (fn l => adjustAptrListBase (oldaptr, newaptr, l)) ll
                val u2 = toSetSet ll2
            in u2
            end  
    end         

(*-------------------------------change esp to ebp--------------------------------------*) 
fun adjustAptrEsp2Ebp aptr = adjustAptrBase ((A.Preg(A.Esp)), (A.Preg(A.Ebp)), aptr)
fun adjustAptrListEsp2Ebp list = adjustAptrListBase ((A.Preg(A.Esp)), (A.Preg(A.Ebp)), list)
fun adjustPexpEsp2Ebp pexp = adjustPexpBase ((A.Preg(A.Esp)), (A.Preg(A.Ebp)), pexp)
fun adjustPpropEsp2Ebp pprop = adjustPpropBase ((A.Preg(A.Esp)),(A.Preg(A.Ebp)), pprop)
fun adjustNDEsp2Ebp set  = adjustNDBase ((A.Preg(A.Esp)), (A.Preg(A.Ebp)), set)
fun adjustPiEsp2Ebp pi = adjustPiBase  ((A.Preg(A.Esp)), (A.Preg(A.Ebp)), pi)
fun adjustUEsp2Ebp u = adjustUBase  ((A.Preg(A.Esp)), (A.Preg(A.Ebp)), u)

(*-------------------------------change ebp to esp--------------------------------------*) 
fun adjustAptrEbp2Esp aptr = adjustAptrBase ((A.Preg(A.Ebp)), (A.Preg(A.Esp)), aptr)
fun adjustAptrListEbp2Esp list = adjustAptrListBase ((A.Preg(A.Ebp)), (A.Preg(A.Esp)), list)
fun adjustPexpEbp2Esp pexp = adjustPexpBase ((A.Preg(A.Ebp)), (A.Preg(A.Esp)), pexp)
fun adjustPpropEbp2Esp pprop = adjustPpropBase ((A.Preg(A.Ebp)),(A.Preg(A.Esp)), pprop)
fun adjustNDEbp2Esp set  = adjustNDBase ((A.Preg(A.Ebp)), (A.Preg(A.Esp)), set)
fun adjustPiEbp2Esp pi = adjustPiBase  ((A.Preg(A.Ebp)), (A.Preg(A.Esp)), pi)
fun adjustUEbp2Esp u = adjustUBase  ((A.Preg(A.Ebp)), (A.Preg(A.Esp)), u)

(*----------------------------------My basic code blocks------------------------*)
type mycb = {label : string
           , code  : A.instr list
           , asst  : A.passert
           , ckflag  : bool
           , iscycle : bool
           , tolabel1 : string
           , tolabel2 : string
            }
val cblks : mycb list ref = ref []

fun getMyCbLab (cb : mycb)= #label cb 
fun getMyCbCode (cb : mycb) = #code cb
fun getMyCbAsst (cb : mycb) = #asst cb
fun getMyCbFlag (cb : mycb) = #ckflag cb
fun getMyCbIsCycle (cb : mycb) = #iscycle cb
fun getMyCbTolabel1 (cb : mycb) = #tolabel1 cb
fun getMyCbTolabel2 (cb : mycb) = #tolabel2 cb

fun setMyCbFlag (cb : mycb, flag) =
    {label = getMyCbLab cb
   , code = getMyCbCode cb
   , asst = getMyCbAsst cb
   , ckflag = flag
   , iscycle = getMyCbIsCycle cb
   , tolabel1 = getMyCbTolabel1 cb
   , tolabel2 = getMyCbTolabel2 cb
    }

fun cbs2mycbs cblks =
    case cblks 
     of [] => []
      | cb::cbs => 
        let val label = A.getCbLab4p cb
            val code = A.getCbCode4p cb
            val asst = A.getCbAsst4p cb
            fun getlabel instr =
                case instr 
                 of A.Jmp(l) => (l, "")
                  | A.Je(l, ln) => (l, ln)
                  | A.Jg(l, ln) => (l, ln)
                  | A.Jge(l, ln) => (l, ln)
                  | A.Malloc(_, l,_) => (l, "")
                  | A.Call (_, l) => (l, "")
                  | A.Ret(l) => ("", "")
                  | _ => (debugPrint ("instruction : "^(A.toString (instr))) 
                        ;raise Fail "basic block ended with non-jmp instrution...\n")
            fun getLabels cd =
                case cd 
                 of instr :: [] => getlabel instr
                  | instr :: instrs => getLabels instrs
                  | [] => raise Fail "basic block constains no instructions ...\n"
            val (l1, l2) = getLabels code
            val cycleflag = case asst
                             of NONE => false
                              | SOME (A.Ptrue) => false
                              | SOME (_) => true
            val str = if cycleflag then " is " else " is not "
            val _ = debugPrint (label^str^" cycle entry...\n")
        in {label = label, code = code, asst = asst, ckflag = false
          , iscycle = cycleflag, tolabel1 = l1, tolabel2 = l2}::(cbs2mycbs cbs)
        end

fun getMyCblkAtLabel (cblks, label) =
    case cblks 
     of [] => NONE
      | cb::cbs => 
        let val label1 = getMyCbLab cb
        in if label1 = label 
           then SOME cb
           else getMyCblkAtLabel (cbs, label)
        end

fun isMyCbChecked (cblk, label) =
    if getMyCbLab cblk = label 
       then getMyCbFlag cblk 
       else true
            
fun isMyCbCheckedInCbs (cblks, label) =
    case cblks 
     of [] => false
      | cb::cbs => 
        if getMyCbLab cb = label 
        then getMyCbFlag cb
        else isMyCbCheckedInCbs (cbs, label)

fun isMyCbCycleEntry (cblk, label) =
    if getMyCbLab cblk = label 
       then getMyCbIsCycle cblk 
       else false
            
fun isMyCbCycleEntryInCbs (cblks,label) =
    let val _ = debugPrint ""
    in case cblks 
        of [] => false
         | cb::cbs => 
           if getMyCbLab cb = label 
           then getMyCbIsCycle cb
           else isMyCbCycleEntryInCbs (cbs, label)
    end

fun isMyCbEntryInCbs (cblks,label) =
    case cblks 
     of [] => false
      | cb::cbs => 
        if getMyCbLab cb = label 
        then true
        else false

fun isMyCbRetInCbs (cblks,label) =
    case cblks 
     of cb::[] => 
        if getMyCbLab cb = label 
        then true
        else false
      | cb::cbs =>
        isMyCbRetInCbs (cbs,label)
      | _ => false

fun setMyCbChecked (cblks, label) =
    case cblks
     of [] => []
      | cb::cbs => 
        if getMyCbLab cb = label
        then (setMyCbFlag (cb, true))::cbs 
        else cb::(setMyCbChecked (cbs, label))

 

(*----------------------------------Program and Basic Blocks---------------------*)
fun fname     prf = (A.getFname prf)
fun fcblks    prf = (A.getCode  prf)
fun fcblksNum prf = Int.toString(List.length (fcblks prf))

fun cblkLabel cblk = (getMyCbLab cblk)
fun cblkCode  cblk = (getMyCbCode cblk)
fun cblkCnum  cblk = Int.toString(List.length (cblkCode cblk))
fun cblkpprop cblk = 
    let val passert = (getMyCbAsst cblk)
    in case passert
        of  NONE =>let val _ = debugPrint "Block passert : NONE \n" 
                   in A.Ptrue 
                   end
         |  SOME pprop => pprop             
    end

(*-----------------------------------Register Judgement--------------------------*)

fun isRegEsp reg = if reg = A.Esp then true else false
fun isRegEbp reg = if reg = A.Ebp then true else false
fun isRegEax reg = if reg = A.Eax then true else false

fun isRegStkreg reg = 
    if isRegEsp reg orelse isRegEbp reg 
    then true 
    else false

fun isRegStkreg2 (reg1, reg2) = 
    if isRegStkreg reg1 orelse isRegStkreg reg2 
    then true 
    else false



(*----------------------------------Temperory Type Contex------------------------*)
type Gamma = (A.aptr * A.etype) list
             
val emp_gamma = []
                
fun getTypeGamma (gamma, aptr) =
    case gamma
     of [] => NONE
      | (x0, t) :: xs => 
        if x0 = aptr
        then SOME t
        else getTypeGamma (xs, aptr)

fun isAptrInGamma (gamma, aptr) =
    case gamma
     of [] => false
      | (x0, t) :: xs => 
        if x0 = aptr
        then true
        else isAptrInGamma (xs, aptr)  

fun setTypeGammaIn (gamma, aptr, etype) = 
    case gamma
     of [] => []
      | (x0, t) :: xs => 
        if x0 = aptr
        then (x0, etype)::xs
        else (x0, t)::(setTypeGammaIn (xs, aptr, etype))  

fun setTypeGamma (gamma, aptr, etype) =
    if isAptrInGamma (gamma, aptr)
    then setTypeGammaIn (gamma, aptr, etype)
    else ((aptr,etype)::gamma)

fun deleteAptrInGamma (gamma, aptr) =
     if isAptrInGamma (gamma, aptr)
     then case gamma
           of [] => []
            | (x0, t) :: xs => 
              if x0 = aptr
              then xs
              else (x0, t)::(deleteAptrInGamma (xs, aptr)) 
    else gamma

fun isAptrAndBase (aptr, aimaptr) = 
    let val _ = adjustDebugPrint "is aptr base \n"  
    in if aptr = aimaptr
       then false
       else case aimaptr
             of A.Preg(reg) => false
              | A.Pstk(off,reg) => 
                if (aptr = A.Preg(reg))
                then true
                else false
              | A.Pmem(off,aptr1,pexp) =>
                if isAptrAndBase (aptr, aptr1)
                then true
                else false
              | A.Pgmem(l) => false
              | A.Pid(str) => false
    end

fun deleteAptrBaseInGamma (gamma, aptr) =
    case gamma
     of [] => []
      | (x0, t) :: xs => 
        if isAptrAndBase (aptr, x0)
        then (adjustDebugPrint ("In "^A.aptr2str(aptr)^"<"^A.aptr2str(x0)^"\n"); (deleteAptrBaseInGamma (xs, aptr)))
        else (adjustDebugPrint ("Not In "^A.aptr2str(aptr)^"<"^A.aptr2str(x0)^"\n"); (x0, t)::(deleteAptrBaseInGamma (xs, aptr)))

fun removeGammaReg gamma = 
    let val g1 = deleteAptrInGamma (gamma, A.Preg(A.Eax))
        val g2 = deleteAptrInGamma (g1, A.Preg(A.Ebx))
        val g3 = deleteAptrInGamma (g2, A.Preg(A.Ecx))
        val g4 = deleteAptrInGamma (g3, A.Preg(A.Edx))
        val g5 = deleteAptrInGamma (g4, A.Preg(A.Esi))
        val g6 = deleteAptrInGamma (g5, A.Preg(A.Edi))
    in g6
    end
(*0(esp) i => -i(esp)*)
fun adjustGamma (gamma, aptr, i) =
    case gamma
     of [] => []
      | (x0, t) :: xs => 
        (adjustAptrSubI (aptr, i, x0), t)::(adjustGamma (xs, aptr, i))

(*0(esp)  => 0(ebp)*)
fun adjustGammaEsp2Ebp gamma  =
    let val _ = adjustDebugPrint "adjust Gamma esp2ebp ... \n"
    in case gamma
        of [] => []
         | (x0, t) :: xs => 
           (adjustAptrEsp2Ebp x0, t)::(adjustGammaEsp2Ebp xs)
    end
(*0(ebp)  => 0(esp)*)
fun adjustGammaEbp2Esp gamma  =
    let val _ = adjustDebugPrint "adjust Gamma esp2ebp ... \n"
    in case gamma
        of [] => []
         | (x0, t) :: xs => 
           (adjustAptrEbp2Esp x0, t)::(adjustGammaEbp2Esp xs)
    end
fun dumpGamma gamma =
    let val _ = ()
    in case gamma
        of [] => ()
         | (x0, t) :: xs => 
           (debugPrint ((A.aptr2str x0)^" : "^(A.etype2str t)^",  ") ;(dumpGamma xs))
    end

and outFail (debuginfo, tctx, env) =
    let val _ = (print ("Asmprover found error in: \n"^(getDebugInfoStr (debuginfo))^"\n"))
        val _ = if showFailEvn then outputInfoFail (tctx, env) else ()
    in raise AsmProverFail
    end

and setPosAndFail (debuginfo, tctx, env, str) : 'a =
    let val dmsg = setDebugPos (debuginfo, str)
    in outFail (dmsg, tctx, env) 
    end

and getTypeAll (tctx, aptr) =
    let val (asmenv, gamma, debuginfo, env) = tctx
        val tctx1 = (asmenv, gamma)
        val res1 = A.getType(aptr,asmenv)
        val res2 = getTypeGamma (gamma, aptr)
        (*fun fail str = setPosAndFail (debuginfo, tctx1, env, str)*)
        fun fail str =  print ("Asmprover found error in: \n"^(getDebugInfoStr (setDebugPos(debuginfo,str)))^"\n")
    in case (res1, res2)
        of (NONE, NONE) => 
           let val _ = debugPrint ((A.aptr2str(aptr))^" No TypeInfo!!\n") 
           in case aptr
               of A.Pstk _ => 
                  (print ("Asmprover found error in: \n"^
                          (getDebugInfoStr (setDebugPos(debuginfo,(A.aptr2str aptr)^" : type infomation does not exist")))^"\n");
                               raise AsmProverFail) (*fail ((A.aptr2str aptr)^" : type infomation does not exist")*)
                | A.Preg _ => A.Int 
                | _ => A.Int
           end
         | (NONE,SOME t) =>
           let val _ = debugPrint ((A.aptr2str aptr)^" has ("^(A.etype2str t)^") TypeInfo in Gamma \n") 
           in t
           end
         | (SOME t, NONE) => 
           let val _ = debugPrint ((A.aptr2str aptr)^" has ("^(A.etype2str t)^") TypeInfo In Asmenv !\n") 
           in t
           end
         | (SOME t1, SOME t2) =>  
           let val _ = debugPrint ((A.aptr2str aptr)^" ("^(A.etype2str t1)^","^(A.etype2str t2)^") TypeInfo In Asmenv & Gamma!\n")
           in if t1 = t2 
              then t1
              else (print ("Asmprover found error in: \n"^
                          (getDebugInfoStr (setDebugPos(debuginfo,"Different type info in asmenv & gamma!")))^"\n");
                    raise AsmProverFail) (*fail ("Different type info in asmenv & gamma!")*)
           end
    end

 and isIntType (tctx, aptr) = 
     if getTypeAll (tctx, aptr) = A.Int
     then true
     else false

 and isIntType2 (tctx, aptr1, aptr2) = 
     if isIntType (tctx, aptr1) andalso isIntType (tctx, aptr2)
     then true
     else false

 and isPtrType (tctx, aptr) = 
     let val t = getTypeAll (tctx, aptr)
     in case t
         of A.Ptr(_) => true
          | _ => false
     end

 and isPtrInPiNDU (pndu, aptr) =
     let val (PiSet, NSet, DSet, USet) = pndu
     in if isPtrInPi (aptr, PiSet) orelse isPtrInN (aptr,NSet) 
           orelse isPtrInD (aptr, NSet) orelse isPtrInU (aptr, USet)
        then true
        else false
     end

 (*in pind => ptr
  Int => not in pind*)
 and isPtrInfoCorrect (tctx, pndu, aptr) = 
     if isPtrInPiNDU (pndu, aptr) (*In PiND*)
     then if (not (isPtrType (tctx, aptr))) 
          then false            
          else true 
     else true 

 and isPtrInfoCorrect2 (tctx, pndu, aptr1, aptr2) =
     if isPtrInfoCorrect (tctx, pndu, aptr1) andalso isPtrInfoCorrect (tctx, pndu, aptr2)
     then true
     else false

(*----------------------------------utils -------------------------------------------------*)

and outputPprop (pprop, flag) =
    let val myPrint = if flag then debugPrint else print
    in case pprop
        of NONE => myPrint "NONE\n"
         | SOME pprop1 => myPrint ((A.pprop2str pprop1)^"\n")   
    end
                    
and outputEnv (env, flag) =
    let val (pprop, PiP, PiSet, NSet, DSet, USet) = env
        val myPrint = if not flag then debugPrint else print
        val _ = (myPrint ("pprop: "^(A.pprop2str pprop)^"\n"))
        val _ = (myPrint ("PiPrd: "^(A.pprop2str PiP)^"\n"))
        val _ = (myPrint ("PiSet: "); printSetset (myPrint, PiSet); myPrint "\n" )                               
        val _ = (myPrint ("N Set: "); printSet (myPrint, NSet); myPrint "\n")
        val _ = (myPrint ("D Set: "); printSet (myPrint, DSet); myPrint "\n") 
        val _ = (myPrint ("U Set: "); printSetset (myPrint, USet); myPrint "\n" )   
    in ()
    end
 
and outputInfoFail (tctx, env) = 
    let val (pprop, PiP, PiSet, NSet, DSet, USet) = env
        val (asmevn, gamma) = tctx 
        val _ = (print ("----Evn Info--------------------------------------------------\n"))
        val _ = outputEnv (env, true)
        val _ = (print ("----ASMEnv:\n"^(A.asmenv2str asmevn)))
        val _ = (print ("----Gamma :\n") ; dumpGamma gamma)
        val _ = (print ("\n-----------------------------------------------Env Info done--\n"))
    in ()
    end

and outputInfo (tctx, env)  = 
    let val (pprop, PiP, PiSet, NSet, DSet, USet) = env
        val (asmevn, gamma) = tctx 
        val _ = (debugPrint ("----Evn Info--------------------------------------------------\n"))
        val _ = outputEnv (env, debugFlag())
        val _ = (if showAsmEnv then debugPrint ("[Asmenv]:\n"^(A.asmenv2str asmevn)) else ())
        val _ = (debugPrint ("[Gamma] :\n") ; dumpGamma gamma)
        val _ = (debugPrint ("\n-----------------------------------------------Env Info done--\n"))
        val _ = debugPrint "[log]\n"
    in ()
    end



(*----------------------------------get checking info----------------------------*)
 datatype ppropty 
   = PSingle
   | POrNPi

 fun getPpropType pprop = 
     let val default = PSingle
     in case pprop
         of A.Ptrue  => default
          | A.Pnot _ => default
          | A.Pand (pprop1, pprop2) => default       
          | A.Por (pprop1, pprop2)  => POrNPi
          | A.Pge (_, _) => default
          | A.Pgt (_, _) => default
          | A.Plt (_, _) => default
          | A.Ple (_, _) => default
          | A.Peq (_, _) => default
          | A.Pne (_, _) => default
          | A.Pforall ((str, etype), pprop) => default
          | A.Pex     ((str, etype), pprop) => default
          | A.Pi (aptrlistlist) =>  default
          | A.N  (aptrlist) => default
          | A.D  (aptrlist) => default
          | A.Ptree pexp  => default
          | A.Plist pexp  => default
          | A.Ppred _     => default
     end

  fun getPiSet pprop = 
      let val emp = emp_pi
      in case pprop
          of A.Ptrue  => (A.Ptrue, emp)
           | A.Pnot _ => (A.Ptrue, emp) 
           | A.Pand (pprop1, pprop2) => 
             let val (pre1,setset1) = getPiSet pprop1
                 val (pre2,setset2) = getPiSet pprop2
                 val pre = if pre1 <> A.Ptrue andalso pre2 <> A.Ptrue 
                           then A.Pand (pre1,pre2) 
                           else (if pre1<> A.Ptrue
                                 then pre1
                                 else pre2)
                 val setset = if isEmptyPi setset1 then setset2 else setset1
             in  (pre,setset)
             end
           | A.Por (pprop1, pprop2)  => (A.Ptrue, emp)          
           | A.Pge (_, _) => (A.Ptrue, emp)
           | A.Pgt (_, _) => (A.Ptrue, emp)
           | A.Plt (_, _) => (A.Ptrue, emp)
           | A.Ple (_, _) => (A.Ptrue, emp)
           | A.Peq (_, _) => (A.Ptrue, emp)
           | A.Pne (_, _) => (A.Ptrue, emp)
           | A.Pforall ((str, etype), pprop) => (A.Pforall ((str,etype),pprop), emp) (*???????*)
           | A.Pex     ((str, etype), pprop) => (A.Pex     ((str,etype),pprop), emp) (*???????*)
           | A.Pi (aptrlistlist) =>  (A.Ptrue, toSetSet aptrlistlist) 
           | A.N  (aptrlist) => (A.Ptrue, emp)
           | A.D  (aptrlist) => (A.Ptrue, emp)
           | A.Ptree pexp  => (A.Ptree pexp, emp)
           | A.Plist pexp  => (A.Plist pexp, emp)
           | A.Ppred _     => (A.Ptrue, emp) (*Not deal with yet*)
      end

    
fun getNDSet (sort, pprop) = 
    let fun selectOne (set1, set2) =
            if isEqN(set1, emp_n) 
            then set2
            else set1
        val emp = if sort = N then emp_n else emp_d 
    in case pprop
        of A.Ptrue => emp
         | A.Pnot _ => emp (*???????*)
         | A.Pand (pprop1, pprop2) => selectOne (getNDSet (sort, pprop1), getNDSet (sort, pprop2))
         | A.Por (pprop1, pprop2)  => emp
         | A.Pge (_, _) => emp
         | A.Pgt (_, _) => emp
         | A.Plt (_, _) => emp
         | A.Ple (_, _) => emp
         | A.Peq (_, _) => emp
         | A.Pne (_, _) => emp
         | A.Pforall _ => emp (*???????*)
         | A.Pex _ => emp (*???????*)
         | A.Pi _ => emp
         | A.N (aptrlist) => if sort = N then toSet (aptrlist) else emp
         | A.D (aptrlist) => if sort = D then toSet (aptrlist) else emp
         | A.Ptree _  => emp
         | A.Plist _  => emp
         | A.Ppred _  => emp
    end

  fun getUSet pprop = 
      let val emp = emp_u
      in case pprop
          of A.Ptrue  => emp
           | A.Pnot _ => emp
           | A.Pand (pprop1, pprop2) => 
             let val setset1 = getUSet pprop1
                 val setset2 = getUSet pprop2
             in PiSet.union (setset1, setset2)
             end
           | A.Por (pprop1, pprop2)  => emp
           | A.Pge (_, _) => emp
           | A.Pgt (_, _) => emp
           | A.Plt (_, _) => emp
           | A.Ple (_, _) => emp
           | A.Peq (_, _) => emp
           | A.Pne (_, _) => emp
           | A.Pforall ((str, etype), pprop1) => getUSet pprop1 (*???????*)
           | A.Pex     ((str, etype), pprop1) => getUSet pprop1 (*???????*)
           | A.Pi (aptrlistlist) => emp 
           | A.N  (aptrlist) => emp
           | A.D  (aptrlist) => emp
           | A.Ptree pexp  => 
             (case pexp
               of A.Pvar(aptr) => addSingletonU (aptr, emp)
                | _ => emp)
           | A.Plist pexp  => 
             (case pexp
               of A.Pvar(aptr) => addSingletonU (aptr, emp)
                | _ => emp)
           | A.Ppred (_)     => emp (*Not deal with yet*)
      end

(*----------------------------------------Env---------------------------------------------*)
    
fun initEnv str =
    let val _ = (debugPrint str)   
        val pprop = A.Ptrue
        val PiP   = A.Ptrue
        val PiSet = emp_pi
        val NSet  = emp_n
        val DSet  = emp_d
        val USet  = emp_u 
    in (pprop, PiP, PiSet, NSet, DSet, USet)
    end

fun splitPprop pprop =
    case (getPpropType pprop)
     of PSingle => raise AsmProverFail
      | POrNPi =>
        let val _ = debugPrint "Splitting the pprop into two...\n"
        in case pprop 
            of A.Por(p1, p2) => (p1, p2)
             | _ => raise AsmProverFail
        end

fun createEnv (str, cblk) =
    let val _ = (debugPrint str)
        val pprop = (cblkpprop cblk)
       
        val _ = (debugPrint ("Entry assertion is : "^(A.pprop2str pprop)^"\n"))
    in case (getPpropType pprop)
        of PSingle => 
           let val _ = debugPrint "@pprop not include or...\n "
               val (PiP,PiSet) = getPiSet pprop
               val NSet = getNDSet (N, pprop)
               val DSet = getNDSet (D, pprop)
               val USet = getUSet pprop
           in ((pprop, PiP, PiSet, NSet, DSet, USet), (A.Ptrue, A.Ptrue, emp_pi, emp_n, emp_d, emp_u))
           end
         | POrNPi => 
            let val _ = debugPrint "@pprop include or...\n "
                val (ppropl, ppropr) = splitPprop pprop
                val (PiPl, PiSetl) = getPiSet ppropl
                val NSetl = getNDSet (N, ppropl)
                val DSetl = getNDSet (D, ppropl)
                val USetl = getUSet ppropl
                val (PiPr, PiSetr) = getPiSet ppropr
                val NSetr = getNDSet (N, ppropr)
                val DSetr = getNDSet (D, ppropr)
                val USetr = getUSet ppropr
            in ((ppropl, PiPl, PiSetl, NSetl, DSetl, USetl), (ppropr, PiPr, PiSetr, NSetr, DSetr, USetr))
            end
    end    

fun adjustEnv (env, aptr, i)  =
    let val (pprop, PiP, PiSet, NSet, DSet, USet) = env
        val newPiSet = adjustPiSubI (aptr, i, PiSet)
        val newNSet  = adjustNDSubI (aptr, i, NSet)
        val newDSet  = adjustNDSubI (aptr, i, DSet)
        val newUSet  = adjustUSubI (aptr, i, USet)
        val newPprop = adjustPpropSubI (aptr, i, pprop)
        val newPiP   = adjustPpropSubI (aptr, i, PiP)
    in (newPprop, newPiP, newPiSet, newNSet, newDSet, newUSet)
    end

fun adjustEnvEsp2Ebp env =
    let val _ = debugPrint "adujust env esp2ebp...\n"
        val (pprop, PiP, PiSet, NSet, DSet, USet) = env
        val newPiSet = (adjustPiEsp2Ebp PiSet)
        val newNSet  = (adjustNDEsp2Ebp NSet)
        val newDSet  = (adjustNDEsp2Ebp DSet)
        val newUSet  = (adjustUEsp2Ebp USet)
        val newPprop = (adjustPpropEsp2Ebp pprop)
        val newPiP   = (adjustPpropEsp2Ebp PiP)
    in (newPprop, newPiP, newPiSet, newNSet, newDSet, newUSet)
    end

fun adjustEnvEbp2Esp env =
    let val _ = debugPrint "adujust env ebp2esp...\n"
        val (pprop, PiP, PiSet, NSet, DSet, USet) = env
        val newPiSet = (adjustPiEbp2Esp PiSet)
        val newNSet  = (adjustNDEbp2Esp NSet)
        val newDSet  = (adjustNDEbp2Esp DSet)
        val newUSet  = (adjustUEbp2Esp USet)
        val newPprop = (adjustPpropEbp2Esp pprop)
        val newPiP   = (adjustPpropEbp2Esp PiP)
    in (newPprop, newPiP, newPiSet, newNSet, newDSet, newUSet)
    end

fun adjustEnvAliasSubst (env, aptr) =
    let val _ = debugPrint "adjust env alias subst begin...\n"
        val (pprop, PiP, PiSet, NSet, DSet, USet) = env
        val aliasaptr = getAnotherPtrSameSetPi (aptr, PiSet)
        val _ = debugPrint ("@aptr : "^A.aptr2str(aptr)^"\n")
        val _ = debugPrint ("@alias aptr : "^A.aptr2str(aliasaptr)^"\n")
        val newPiSet  = adjustPiBase (aptr, aliasaptr, PiSet)
        val newNSet   = adjustNDBase (aptr, aliasaptr, NSet)
        val newDSet   = adjustNDBase (aptr, aliasaptr, DSet)
        val newUSet   = adjustUBase (aptr, aliasaptr, USet)
        val newPprop  = adjustPpropBase (aptr, aliasaptr, pprop)
        val newPiP    = adjustPpropBase (aptr, aliasaptr, PiP)
        val newenv = (pprop, PiP, newPiSet, newNSet, newDSet, newUSet)
        val _ = debugPrint "adjust env alias subst end...\n"
    in newenv
    end

fun adjustEnvSubstAndDeletePi (env, oldaptr, newaptr) =
    let val (pprop, PiP, PiSet, NSet, DSet, USet) = env
        val aliasaptr = newaptr
        val pi1 = addPtrPi (newaptr, oldaptr, PiSet)
        val pi2 = deletePtrPi (oldaptr, pi1)
        val newPiSet  = adjustPiBase (oldaptr, aliasaptr, pi2)
        val newNSet   = adjustNDBase (oldaptr, aliasaptr, NSet)
        val newDSet   = adjustNDBase (oldaptr, aliasaptr, DSet)
        val newUSet   = adjustUBase (oldaptr, aliasaptr, USet)
        val newPprop  = adjustPpropBase (oldaptr, aliasaptr, pprop)
        val newPiP    = adjustPpropBase (oldaptr, aliasaptr, PiP)
    in (pprop, PiP, newPiSet, newNSet, newDSet, newUSet)
    end

fun adjustEnvSubstAndDeleteU (env, oldaptr, newaptr) =
    let val (pprop, PiP, PiSet, NSet, DSet, USet) = env
        val aliasaptr = newaptr
        val u1 = addPtrPi (newaptr, oldaptr, USet)
        val u2 = deletePtrU (oldaptr, u1)
        val newPiSet  = adjustPiBase (oldaptr, aliasaptr, PiSet)
        val newNSet   = adjustNDBase (oldaptr, aliasaptr, NSet)
        val newDSet   = adjustNDBase (oldaptr, aliasaptr, DSet)
        val newUSet   = adjustUBase (oldaptr, aliasaptr, u2)
        val newPprop  = adjustPpropBase (oldaptr, aliasaptr, pprop)
        val newPiP    = adjustPpropBase (oldaptr, aliasaptr, PiP)
    in (newPprop, newPiP, newPiSet, newNSet, newDSet, newUSet)
    end

fun adjustEnvNotLeaking (env, rsaptr, rdaptr) =
    let val (pprop, PiP, PiSet, NSet, DSet, USet) = env
        val rsset = getPtrSetItem (rsaptr, PiSet) (*rs.eq*)
        val _ = (debugPrint "@rs.eq:"; printSet (debugPrint, rsset)) 
        val pi0 = deleteSetPi (rsset, PiSet)  (*Pi - rs.eq*)
        val _ = (debugPrint "@Pi - rs.eq :"; printSetset (debugPrint, pi0))
        val rdalias = getAnotherPtrSameSetPi (rdaptr, PiSet)
        val _ = debugPrint ("@rdalias:"^A.aptr2str(rdalias)^"\n")
        val newrsset = addPtrN (rdaptr, adjustNDBase (rdaptr, rdalias, rsset)) (*rs.eq/rd +{rd}*)
        val _ = (debugPrint "@new rs.eq:"; printSet (debugPrint, newrsset))
        val (newPprop, newPiP, newPi, newN, newD, newU) = 
            adjustEnvAliasSubst ((pprop, PiP, pi0, NSet, DSet, USet), rdaptr)
        val pi1 = deletePtrPi (rdaptr, newPi) (*Pi-rs.eq /rd -rd*)
        val newPiSet = addSetPi (newrsset, pi1)(*Pi-rs.eq/rd -rd + {rs.eq/rd+{rd}}*)            
    in (newPprop, newPiP, newPiSet, newN, newD, newU)
    end 

fun adjustEvnNotLeakingSubstAndDeleteRsPi (env, rsaptr, rdaptr) =
    let val (pprop, PiP, PiSet, NSet, DSet, USet) = env
        val rsset = getPtrSetItem (rsaptr, PiSet) (*rs.eq*)
        val pi0 = deleteSetPi (rsset, PiSet)  (*Pi - rs.eq*)
        val rdalias = getAnotherPtrSameSetPi (rdaptr, PiSet)
        val newrsset = addPtrN (rdaptr, adjustNDBase (rdaptr, rdalias, rsset)) (*rs.eq/rd +{rd}*)
        val (newPprop, newPiP, newPi, newN, newD, newU) = 
            adjustEnvAliasSubst ((pprop, PiP, pi0, NSet, DSet, USet), rdaptr)
        val pi1 = deletePtrPi (rdaptr, newPi) (*Pi-rs.eq /rd -rd*)
        val pi2 = addSetPi (newrsset, pi1)(*Pi-rs.eq/rd -rd + {rs.eq/rd+{rd}}*)  
        val (Pprop0, PiP0, Pi0, N0, D0, U0) = 
            adjustEnvAliasSubst ((newPprop, newPiP, pi2, newN, newD, newU), rsaptr)
        val pi3 = deletePtrPi (rsaptr, Pi0)          
    in (Pprop0, PiP0, pi3, N0, D0, U0)
    end 

fun adjustEnvU2N (aptr, env) =
    let val _ = debugPrint ("adjust env u to n...\n")
        val (pprop, PiP, PiSet, NSet, DSet, USet) = env
    in if isPtrInU (aptr, USet)
       then let val aptrset = getPtrSetItem (aptr, USet)
                val newUSet = deleteSetU (aptrset, USet)
                val newNSet = NDSet.union (NSet, aptrset)
            in (pprop, PiP, PiSet, newNSet, DSet, newUSet)
            end
       else env
    end

fun adjustEnvU2Pi (aptr, env) =
    let val _ = debugPrint ("adjust env u to pi...\n")
        val (pprop, PiP, PiSet, NSet, DSet, USet) = env
    in if isPtrInU (aptr, USet)
       then let val aptrset = getPtrSetItem (aptr, USet)
                val newUSet = deleteSetU (aptrset, USet)
                val newPiSet = addSetPi (aptrset, PiSet)
            in (pprop, PiP, newPiSet, NSet, DSet, newUSet)
            end
       else env
    end

(*-------------------------------------------Checking imply relationship------------------------*)

fun isSetMemberAllReg testset =
    let val l = toList testset
        fun checkList ll =
            case ll
             of [] => true
              | aptr::lls =>
                (case aptr 
                  of A.Preg(_) => checkList lls
                   | _ => false)
    in checkList l
    end

(*remove aptr from list l*)
fun removeListItem (l, aptr) =
    case l
     of [] => []
      | aptr1::l1 =>
        if aptr = aptr1
        then removeListItem (l1, aptr)
        else aptr1::(removeListItem (l1, aptr))

(*len l1 > len l2*)
(*return a list which contains the items not in list l2*)
fun getDiffItemList (l1, l2) = 
    case l2 
     of [] => l1
      | aptr::l21 =>
        getDiffItemList (removeListItem(l1, aptr), l21)

(*check whether the set contains only register aptr*)
fun checkSetDiffReg (set1, set2) =
    let val size1 = NDSet.numItems set1
        val size2 = NDSet.numItems set2
        val l1 = toList set1
        val l2 = toList set2
    in if isEqN (set1, set2)
       then true
       else let val _ = debugPrint "two sets are not equal\n"
                val difflist = 
                    if size1 > size2 
                    then getDiffItemList (l1, l2)
                    else getDiffItemList (l2, l1)
                val diffset = toSet difflist
                (*val _ = (debugPrint ("The difference set is : ")
                       ; printSet (debugPrint, diffset)
                       ; debugPrint "\n")*)
            in isSetMemberAllReg diffset
            end
    end

 (*NDSet N1<=N2*)
 fun checkNinN (n1, n2) =
     let val l1 = toList n1
         val l2 = toList n2
     in if (List.length l1) > (List.length l2)
        then false
        else case l1
              of [] => true
               | x::xs =>
                 if isPtrInN (x, n2)
                 then checkNinN(toSet xs, n2)
                 else false
     end

fun checkAllAptrSingle (alist, pndu) =
    case alist
     of [] => []
      | aptr::alist1 =>
        let val _ = debugPrint ("@@"^A.aptr2str(aptr)^"")
        in if isPtrInPiNDU (pndu, aptr) 
           then case (getPtrSort(aptr, pndu))
                 of P => 
                    if isAptrReg (aptr) 
                    then (debugPrint("P1\n"); 1::(checkAllAptrSingle (alist1, pndu)))     
                    else (debugPrint("P0\n"); 0::(checkAllAptrSingle (alist1, pndu)))
                  | N => 
                    if isAptrReg (aptr) 
                    then (debugPrint("N1\n"); 1::(checkAllAptrSingle (alist1, pndu))) 
                    else (debugPrint("N1\n"); 1::(checkAllAptrSingle (alist1, pndu)))
                  | D => 
                    if isAptrReg (aptr) 
                    then (debugPrint("D1\n"); 1::(checkAllAptrSingle (alist1, pndu)))
                    else (debugPrint("D0\n"); 0::(checkAllAptrSingle (alist1, pndu))) 
                  | U => 
                    if isAptrReg (aptr) 
                    then (debugPrint("U1\n"); 1::(checkAllAptrSingle (alist1, pndu)))
                    else (debugPrint("U1\n"); 1::(checkAllAptrSingle (alist1, pndu)))
           else (debugPrint("X0\n"); 0::(checkAllAptrSingle (alist1, pndu)))
        end
(*check single imply relationship*)
fun checkSingleNSetImply (outenv, homeenv) = 
    let val _ = debugPrint ("@Checking single imply relationship of N Set...\n")
        val (pprop, PiP, PiSet, NSet, DSet, USet) = outenv
        val (opprop, oPip, oPiSet, oNSet, oDSet, oUSet) = homeenv
        val pndu = (PiSet, NSet, DSet, USet)
        val pndu2 = (oPiSet, oNSet, oDSet, oUSet)
        val _ = outputPiNDU pndu (debugFlag())
        val _ = outputPiNDU pndu2 (debugFlag())
    in if isEmptyN oNSet
       then true
       else let val _ = debugPrint ("@NSet at home is not empty...\n")
            in if isEqN (NSet, oNSet)
               then (debugPrint ("@NSet oNSet is equal...\n");true)                                      
               else let val _ = debugPrint ("@NSet oNSet is not equal...\n")                       
                        val checklist = checkAllAptrSingle (toList oNSet, pndu)
                        val n = List.foldl (op +) 0 checklist
                        val len = List.length checklist
                    in if len = n
                       then let val _ = debugPrint ("@ len :"^Int.toString(len)^", n :"^Int.toString(n)^"\n")
                                val _ = (debugPrint ("@oNSet:"); printSet(debugPrint, oNSet))
                                val _ = (debugPrint ("@ NSet:"); printSet(debugPrint, NSet))
                            in true (*checkNinN (oNSet, NSet)*)
                            end
                       else false
                    end
            end
    end

(*check DSet imply relationship*)
fun checkSingleDSetImply (outenv, homeenv) =
    let val _ = debugPrint ("@Checking single imply relationship of D Set...\n")
        val (pprop, PiP, PiSet, NSet, DSet, USet) = outenv
        val pndu = (PiSet, NSet, DSet, USet)
        val (opprop, oPip, oPiSet, oNSet, oDSet, oUSet) = homeenv
    in if isEmptyD oDSet
       then true
       else false
    end

fun checkNinNExceptReg (n1, n2) =
     let val l1 = toList n1
         val l2 = toList n2
     in case l1
         of [] => true
          | x::xs =>
            if isPtrInN(x, n2) orelse isAptrReg(x) 
            then (debugPrint (A.aptr2str(x)^"-Y\n") ;checkNinNExceptReg(toSet xs, n2))
            else (debugPrint (A.aptr2str(x)^"-N\n") ;false)
     end

(*check piset imply relationship*)
fun checkSinglePiSetImply (outenv, homeenv) = 
    let val _ = debugPrint ("@Checking imply relationship of Pi Set...\n")
        val (pprop, PiP, PiSet, NSet, DSet, USet) = outenv
        val pndu = (PiSet, NSet, DSet, USet)
        val (opprop, oPip, oPiSet, oNSet, oDSet, oUSet) = homeenv
    in if isEmptyPi oPiSet
       then true
       else let val _ = debugPrint ("@Pi Set at home is not empty...\n")
                val pilist = (PiSet.listItems oPiSet)
                val result = ref true
                fun checkSet pisetlist = 
                    case pisetlist
                     of [] => true
                      | x::xs =>
                        let val setofpi = x (*(List.hd pilist)*)
                            val list = toList setofpi
                            val aptr = List.hd list
                            val set = case getPtrSort(aptr, pndu)
                                       of P => set2elem (getPtrSet (aptr, PiSet))
                                        | U => set2elem (getPtrSet (aptr, USet))
                                        | _ => (print "Cycle invariant imply relationship is wrong!"; raise AsmProverFail)
                            val noregpi = deleteNDBaseReg setofpi
                            val noregset = deleteNDBaseReg set      
                            val _ = debugPrint "@\n"        
                            val _ = printSet (debugPrint, noregpi)
                            val _ = printSet (debugPrint, noregset)
                            val _ = debugPrint "#\n"
                        in if isEqN (noregpi, noregset) 
                           then checkSet xs
                           else false
                        end  
                val re = (checkSet pilist)
            in re
            end
    end

(*check U Set imply relationship*)
fun checkSingleUSetImply (outenv, homeenv) = 
    let val _ = debugPrint ("@Checking single imply relationship of U Set...\n")
        val (pprop, PiP, PiSet, NSet, DSet, USet) = outenv
        val pndu = (PiSet, NSet, DSet, USet)
        val (opprop, oPip, oPiSet, oNSet, oDSet, oUSet) = homeenv
    in if isEmptyU oUSet
       then true
       else if isEqU (USet, oUSet)
            then true 
            else let val _ = debugPrint ("@U Set at home is not empty...\n")
                     val usetlist = (PiSet.listItems oUSet)
                     fun checkAllSet (setlist, pndu) =
                         case setlist
                          of [] => true
                           | set::setlist1 =>
                             let val aptr = List.hd (toList set)
                                 val (p, n, d, u) = pndu
                             in if isPtrInPiNDU (pndu, aptr) 
                                then (debugPrint ("@@ wrong USet\n"); false)
                                else checkAllSet(setlist1, pndu)
                             end
                 in checkAllSet (usetlist, pndu)
                 end
    end
(*check imply relationship between Pi N D U Set*)
fun checkSinglePNDUImply (outenv, homeenv) =
    let val _ = debugPrint ("Checking single imply relationship of Pi N D U Set...\n")
        val (pprop, PiP, PiSet, NSet, DSet, USet) = outenv
        val (opprop, oPip, oPiSet, oNSet, oDSet, oUSet) = homeenv
    in if checkSingleNSetImply (outenv, homeenv)
       then if checkSingleDSetImply (outenv, homeenv)
            then if checkSinglePiSetImply (outenv, homeenv)
                 then if checkSingleUSetImply (outenv, homeenv)
                      then true
                      else (debugPrint ("Single USet imply relationship is wrong\n"); false)               
                 else (debugPrint ("Single PiSet imply relationship is wrong\n"); false)
            else (debugPrint ("Single DSet imply relationship is wrong\n"); false)
       else (debugPrint ("Single NSet imply relationship is wrong\n"); false)
    end


fun getAptrAndTypeList (pip) =
    case pip
        of A.Ptrue        => []
         | A.Pnot(p)      => []
         | A.Pand(p1, p2) => (getAptrAndTypeList p1)@(getAptrAndTypeList p2)
         | A.Por(p1, p2)  => (getAptrAndTypeList p1)@(getAptrAndTypeList p2)
         | A.Ptree(pe)    =>
           (case pe 
             of A.Pvar(aptr) => (aptr, A.Ptr(A.Str "tree"))::[]
              | _ => []
           )
         | A.Plist(pe)    =>
           (case pe 
             of A.Pvar(aptr) => (aptr, A.Ptr(A.Str "list"))::[]
              | _ => []
           )
         | _ => []

fun changeGammaForUSet (tctx, PiP) =
    let val (asmenv, gamma) = tctx
        val aptrtypelist = getAptrAndTypeList PiP
        fun newGamma (g, list) = 
            case list 
             of [] => g
              | (a,t)::list1 =>
                newGamma (setTypeGamma (g, a, t), list1)
    in newGamma (gamma, aptrtypelist)
    end 

(*-------------------------------------------Internal Results-------------------------------------*)
val emp_results = []
type resulttype = (Gamma * A.pprop * A.pprop * PiSet.set * NDSet.set * NDSet.set * PiSet.set)
type resultlisttype = ((string * string) * resulttype) list
val inter_results : resultlisttype ref = ref []
fun initResult str =
    let val _ = debugPrint str
    in (inter_results := emp_results)
    end

fun isLLInResult (l1, l2, relist) =
    case relist 
     of [] => false
      | ((la, lb), result)::ll => 
        if (l1, l2) = (la, lb) 
        then true 
        else isLLInResult (l1, l2, ll)

fun isInResult (l1, l2) = 
    let val relist = !inter_results
    in isLLInResult (l1, l2, relist)
    end

fun setResultNotIn (l1, l2, result) =
    let val relist = !inter_results
    in ((l1, l2), result)::relist
    end

fun setResult (l1, l2, result) =
    let val relist = !inter_results
    in if isLLInResult (l1, l2, relist)
       then raise Fail "internal results already exists, bug"
       else (inter_results := setResultNotIn (l1, l2, result))
    end

fun getResultIn (l1, l2, relist) =
    case relist 
     of [] => raise Fail "impossible"
      | ((la, lb), result)::ll => 
        if (l1, l2) = (la, lb) 
        then result
        else getResultIn (l1, l2, ll)

fun getResult (l1, l2) = 
    let val relist = !inter_results
    in if isLLInResult (l1,l2, relist)
       then getResultIn (l1, l2, relist)
       else raise Fail "bug"
    end

fun dumpResultIn relist =
    case relist
     of [] => ()
      | ((la, lb), (gamma, pprop, pip, piset, nset, dset, uset))::ll =>
        (debugPrint (la^" -> "^lb^" : \n");
         dumpGamma gamma;
         debugPrint "\n";
         outputEnv ((pprop, pip, piset, nset, dset, uset), false);
         dumpResultIn ll)

fun dumpResult str =
    let val _ = debugPrint (str^"\n")
        val relist = !inter_results
    in if showInternalResult 
       then (dumpResultIn relist)
       else ()
    end

fun getFatherOf (cblks, label) =
    if label = ""
    then []
    else case cblks
          of [] => []
           | cblk::cblkss =>
             let val blklabel = getMyCbLab cblk 
                 val tolabel1 = getMyCbTolabel1 cblk
                 val tolabel2 = getMyCbTolabel2 cblk
             in if tolabel1 = label orelse tolabel2 = label
                then blklabel::(getFatherOf (cblkss, label))
                else (getFatherOf (cblkss, label))
             end



(*---------------------------------Checking functions---------------------------------------------*)

(*Addz i rd *)                                (*-=DoNe=-*)
(*@ rd = ebp                ==> Fail
  @ rd = esp or rd in PiSet ==> adjust Pi N D ...
 *)
fun ckAddz (inf, debuginfo, tctx, env, i, rd) =
    let val (pprop, PiP, PiSet, NSet, DSet, USet) = env
        val (asmenv, gamma) = tctx
        val tctx1 = (asmenv, gamma, debuginfo, env) 
        val pndu = (PiSet, NSet, DSet, USet)
        val aptr  = A.Preg(rd)
        val astr  = A.aptr2str(aptr)
        val mylabel = getDebugLabel debuginfo
        val _ = outputInfo (tctx, env)
        fun fail (str : string)  = setPosAndFail (debuginfo, tctx, env, str)
    in  if (isRegEbp rd)                                                        (*rd = EBP => Fail*)
        then fail (astr^" trying to compute with ebp...")
        else if (isRegEsp rd)                                                   (*rd = ESP => adjust gamma Env*)
             then if isMyCbRetInCbs (!cblks, mylabel)
                  then let fun deleteOneVarible ((g, env), espindex) =
                               let val aptr = A.Pstk(0-12-espindex,A.Ebp)
                                   val astr = A.aptr2str(aptr)
                                   val tp = getTypeAll (tctx1, aptr)
                                   val gamma = deleteAptrInGamma (g, aptr)
                                   val (pprop, pip, pi, n, d, u) = env
                                   val pndu = (pi, n, d, u)
                               in case tp 
                                   of A.Int => 
                                      let val _ = debugPrint (astr^" is int, delete from Gamma...\n")
                                      in (gamma, env)
                                      end
                                    | A.Ptr(_) =>
                                      let val _ = debugPrint (astr^" is ptr, delete from Gamma & Pi N D U...\n")
                                      in (case (getPtrSort (aptr, pndu))
                                           of P =>
                                              let val _ = debugPrint (astr^" is in Pi...\n")
                                              in if not_leaking (aptr, pi)
                                                 then let val _ = debugPrint (astr^" is not in singleton Pi...\n")
                                                          val (newPprop, newPiP, newPi, newN, newD, newU)
                                                            = adjustEnvAliasSubst (env, aptr)
                                                          val newPiSet = deletePtrPi (aptr, newPi)
                                                      in (gamma, (newPprop, newPiP, newPiSet, newN, newD, newU))  
                                                      end                                             
                                                 else fail (astr^" is in singleton pi... memory leaking...") 
                                              end
                                            | N =>
                                              let val _ = debugPrint (astr^" is in N Set...\n")
                                                  val newNSet = deletePtrN (aptr, n)
                                              in  (gamma, (pprop, pip, pi, newNSet, d, u))
                                              end
                                            | D =>
                                              let val _ = debugPrint (astr^" is in D Set...\n")
                                                  val newDSet = deletePtrD (aptr, DSet)
                                              in (gamma, (pprop, pip, pi, n, newDSet, u))
                                              end
                                            | U => 
                                              let val _ = debugPrint (astr^" is in U Set...\n")
                                                  val newUSet = deletePtrU (aptr, USet)
                                              in (gamma, (pprop, pip, pi, n, d, newUSet))
                                              end)
                                      end       
                                    | _ => fail ("non int nor ptr... not allowed") 
                               end
                           fun deleteLocalVariable (gamma, env, low, hi) =
                               let fun loop (g, e, min, max) = 
                                       if  min <= max
                                       then let val (ng, ne)=  deleteOneVarible ((g, e), min)
                                            in loop (ng, ne, min+4, max)
                                            end
                                       else (g, e, 0)
                               in loop (gamma, env, low, hi)
                               end
                           val (gamma1, env1, _) = deleteLocalVariable (gamma, env, 4, i)
                           val newgamma = adjustGamma (gamma1, (A.Preg(A.Esp)), i)
                       in ((asmenv, newgamma), adjustEnv (env1, aptr, i))
                       end
                  else let val _ = debugPrint "@remove parameter...\n"
                           fun deleteOneParameter ((g, env), espindex) =
                               let val aptr = A.Pstk(espindex,A.Esp)
                                   val astr = A.aptr2str(aptr)
                                   val tp = getTypeAll (tctx1, aptr)
                                   val gamma = deleteAptrInGamma (g, aptr)
                                   val (pprop, pip, pi, n, d, u) = env
                                   val pndu = (pi, n, d, u)
                               in case tp 
                                   of A.Int => 
                                      let val _ = debugPrint (astr^" is int, delete from Gamma...\n")
                                      in (gamma, env)
                                      end
                                    | A.Ptr(_) =>
                                      let val _ = debugPrint (astr^" is ptr, delete from Gamma & Pi N D U...\n")
                                      in (case (getPtrSort (aptr, pndu))
                                           of P =>
                                              let val _ = debugPrint (astr^" is in Pi...\n")
                                              in if not_leaking (aptr, pi)
                                                 then let val _ = debugPrint (astr^" is not in singleton Pi...\n")
                                                          val (newPprop, newPiP, newPi, newN, newD, newU)
                                                            = adjustEnvAliasSubst (env, aptr)
                                                          val newPiSet = deletePtrPi (aptr, newPi)
                                                      in (gamma, (newPprop, newPiP, newPiSet, newN, newD, newU))  
                                                      end                                             
                                                 else fail (astr^" is in singleton pi... memory leaking...") 
                                              end
                                            | N =>
                                              let val _ = debugPrint (astr^" is in N Set...\n")
                                                  val newNSet = deletePtrN (aptr, n)
                                              in  (gamma, (pprop, pip, pi, newNSet, d, u))
                                              end
                                            | D =>
                                              let val _ = debugPrint (astr^" is in D Set...\n")
                                                  val newDSet = deletePtrD (aptr, DSet)
                                              in (gamma, (pprop, pip, pi, n, newDSet, u))
                                              end
                                            | U => 
                                              let val _ = debugPrint (astr^" is in U Set...\n")
                                                  val newUSet = deletePtrU (aptr, USet)
                                              in (gamma, (pprop, pip, pi, n, d, newUSet))
                                              end)
                                      end       
                                    | _ => fail ("non int nor ptr... not allowed") 
                               end
                           fun deleteParameter (gamma, env, low, hi) =
                               let fun loop (g, e, min, max) = 
                                       if  min <= max
                                       then let val (ng, ne)=  deleteOneParameter ((g, e), min)
                                            in loop (ng, ne, min+4, max)
                                            end
                                       else (g, e, 0)
                               in loop (gamma, env, low, hi)
                               end
                           val (gamma1, env1, _) = deleteParameter (gamma, env, 0, i-4)
                           val newgamma = adjustGamma (gamma1, (A.Preg(A.Esp)), i)
                       in ((asmenv, newgamma), adjustEnv (env1, aptr, i))
                       end
             else if not (isPtrInfoCorrect (tctx1, pndu, aptr))                  (* PtrInfo wrong  => Fail*)
                  then fail (astr^" Ptr Info not correct...")
                  else if isIntType (tctx1, aptr)                                (*rd is Int => no change*)
                       then (tctx, env)
                       else fail (astr^" try to compute with ptr...not allowed...")
    end

(*Addr rs rd*)                                (*-=DoNe=-*)
(*@ rs or rd is esp/ ebp    ==> Fail
  @ rd and rs is Integer    ==> No Change ...
  @ else                    ==> Fail
 *)
fun ckAddr (inf, debuginfo, tctx, env, rs, rd) =
    let val (pprop, PiP, PiSet, NSet, DSet, USet) = env
        val (asmenv, gamma) = tctx
        val tctx1 = (asmenv, gamma, debuginfo, env) 
        val (rsaptr, rdaptr) = (A.Preg(rs),A.Preg(rd))
        val (rsastr, rdastr) = (A.aptr2str(rsaptr),A.aptr2str(rdaptr))
        val _ = outputInfo (tctx, env) (*Output Info*)
        val fail = fn str => setPosAndFail (debuginfo, tctx, env, str)
    in  if isRegStkreg2 (rs, rd)       (*rs rd is stack ptr  => Fail*)
        then fail (rsastr^" or "^rdastr^"  is ESP/EBP... not allowed...")
        else if isIntType2 (tctx1, rsaptr, rdaptr) (*rs rd is both integer  => no change*)
             then (tctx, env)
             else fail (rsastr^" or "^rdastr^" not both integer ... not allowed...")
    end
 
(*Addm i(rs) rd*)                                (*-=DoNe=-*)
(*@ rd is esp/ ebp          ==> Fail
  @ rd and rs is Integer    ==> No Change ...
  @ else                    ==> Fail
 *)
fun ckAddm (inf, debuginfo, tctx, env, i, rs, rd) =
    let val (pprop, PiP, PiSet, NSet, DSet, USet) = env
        val (asmenv, gamma) = tctx
        val tctx1 = (asmenv, gamma, debuginfo, env) 
        val (rsaptr, rdaptr) = (A.Pstk(i,rs), A.Preg(rd))
        val (rsastr, rdastr) = (A.aptr2str(rsaptr),A.aptr2str(rdaptr))
        val _ = outputInfo (tctx, env) (*Output Info*)
        val fail = fn str => setPosAndFail (debuginfo, tctx, env, str)
    in  if isRegStkreg (rd)       (* rd is stack ptr  => Fail*)
        then fail (rdastr^"  is ESP/EBP... not allowed...")
        else if isIntType2 (tctx1, rsaptr, rdaptr) (*rs rd is both integer  => no change*)
             then (tctx, env)
             else fail (rsastr^" or "^rdastr^" not both integer ... not allowed...")
    end

(*Subz i rd*)                                  (*-=DoNe=-*)
(*@ rd = ebp                ==> Fail
  @ rd = esp or rd in PiSet ==> adjust Pi N D ...
 *)
fun ckSubz (inf, debuginfo, tctx, env, i, rd) = 
    let val (pprop, PiP, PiSet, NSet, DSet, USet) = env
        val (asmenv, gamma) = tctx
        val tctx1 = (asmenv, gamma, debuginfo, env) 
        val pndu = (PiSet, NSet, DSet, USet)
        val aptr = A.Preg(rd)
        val astr = A.aptr2str(aptr)
        val atp  = getTypeAll (tctx1, aptr)
        val _ = outputInfo (tctx, env) (*Output Info*)
        val fail = fn str => setPosAndFail (debuginfo, tctx, env, str)
    in  if (isRegEbp rd)          (*rd = EBP => Fail*)
        then fail (astr^" trying to compute with ebp...")
        else if (isRegEsp rd)     (*rd = ESP => adjust gamma Env //local variables*)
             then let val gamma1 = adjustGamma (gamma, (A.Preg(A.Esp)), (~i))
                      val (pprop1, PiP1,PiSet1, NSet1, DSet1, USet1) = adjustEnv (env, aptr, (~i))
                      fun addOneVarible ((g, d), espindex) =
                          let val aptr = A.Pstk(0-12-espindex,A.Ebp)
                              val tp = getTypeAll (tctx1, aptr)
                              val newg = setTypeGamma (g, aptr, tp)
                              val newd = if isPtrType (tctx1, aptr) then addPtrD (aptr, d) else d
                          in (newg, newd)
                          end
                      fun addLocalVariable (gamma, dset, low, hi) =
                          let fun loop (g, d, min, max) = 
                                  if  min <= max
                                  then let val (ng, nd)=  addOneVarible ((g, d), min)
                                       in loop (ng, nd, min+4, max)
                                       end
                                  else (g, d, 0)
                          in loop (gamma, DSet, low, hi)
                          end
                      val (newgamma, newdset, _) = addLocalVariable (gamma1, DSet1, 4, i)
                  in ((asmenv, newgamma), (pprop1, PiP1, PiSet1, NSet1, newdset, USet1))
                  end
             else case atp
                   of A.Int =>   (*rd is Int => no change*)
                      (tctx, env)
                    | A.Ptr(_) =>(* PtrInfo wrong  => Fail*)
                      if not (isPtrInfoCorrect (tctx1, pndu, aptr)) 
                      then fail (astr^" Ptr Info not correct...bug...")
                      else fail (astr^" try to compute with ptr...not allowed...")
                    | _ => fail (astr^" try to compute with non-integer ... not allowed...")                           
    end

(*Subr rs rd*)                                 (*-=DoNe=-*)
(*@ rs or rd is esp/ ebp    ==> Fail
  @ rd and rs is Integer    ==> No Change ...
  @ else                    ==> Fail
 *)
(*as same as checking addr*)
fun ckSubr (inf, debuginfo, tctx, env, rs, rd) = ckAddr (inf, debuginfo, tctx, env, rs, rd) 
   
(*Subm i(rs) rd*)                                (*-=DoNe=-*)
(*@ rd is esp/ ebp          ==> Fail
  @ rd and rs is Integer    ==> No Change ...
  @ else                    ==> Fail
 *)
fun ckSubm (inf, debuginfo, tctx, env, i, rs, rd) = ckAddm (inf, debuginfo, tctx, env, i, rs, rd)

(*Mulz i rd*)                                   (*-=DoNe=-*)
(*@ rd = ebp esp              ==> Fail
  @ rd is PTR or rd in PiSet  ==> Fail
 *)   
fun ckMulz (inf, debuginfo, tctx, env, i, rd) =
    let val (pprop, PiP, PiSet, NSet, DSet, USet) = env 
        val (asmenv, gamma) = tctx
        val tctx1 = (asmenv, gamma, debuginfo, env) 
        val pndu = (PiSet, NSet, DSet, USet)
        val aptr  = A.Preg(rd)
        val astr  = A.aptr2str(aptr)
        val atp  = getTypeAll (tctx1, aptr)
        val _ = outputInfo (tctx, env) (*Output Info*)
        val fail = fn str => setPosAndFail (debuginfo, tctx, env, str)
    in  if isRegStkreg rd      (* rd = ESP or  EBP => Fail*)
        then fail (astr^" trying to compute with esp/ebp...")
        else case atp
              of A.Int =>   (*rd is Int => no change*)
                 (tctx, env)
               | A.Ptr(_) =>(* PtrInfo wrong  => Fail*)
                 if not (isPtrInfoCorrect (tctx1, pndu, aptr)) 
                 then fail (astr^" Ptr Info not correct...bug...")
                 else fail (astr^" try to compute with ptr...not allowed...")
               | _ => fail (astr^" try to compute with non-integer ... not allowed...")                  
    end

(*Mulr rs rd*)                                   (*-=DoNe=-*)
(*@ rs or rd = ebp/esp        ==> Fail
  @ rs or rd is PTR           ==> Fail
 *)   
fun ckMulr (inf, debuginfo, tctx, env, rs, rd) =
    let val (pprop, PiP, PiSet, NSet, DSet, USet) = env
        val (asmenv, gamma) = tctx
        val tctx1 = (asmenv, gamma, debuginfo, env) 
        val pndu = (PiSet, NSet, DSet, USet)
        val (rsaptr, rdaptr) = (A.Preg(rs),A.Preg(rd))
        val (rsastr, rdastr) = (A.aptr2str(rsaptr),A.aptr2str(rdaptr))
        val (rstp, rdtp) = (getTypeAll (tctx1, rsaptr), getTypeAll (tctx1, rdaptr))
        val _ = outputInfo (tctx, env) (*Output Info*)
        val fail = fn str => setPosAndFail (debuginfo, tctx, env, str)
    in  if isRegStkreg2 (rs, rd)       (* rs rd = ESP or EBP => Fail*)
        then fail (rsastr^" or "^rdastr^" trying to compute with esp/ebp...")
        else case (rstp, rdtp)
              of (A.Int, A.Int) => (*rs rd is Int => no change*)
                 (tctx, env)
               | (_ , A.Ptr(_)) => 
                 fail (rdastr^" try to compute with ptr...not allowed...")
               | (A.Ptr(_), _) =>
                 fail (rsastr^" try to compute with ptr...not allowed...")
               | (_, _) =>
                 fail (" non-integer type... not allowed")                
    end

(*Nm i(rs) rd*)                                (*-=DoNe=-*)
(*@ rd is esp/ ebp          ==> Fail
  @ rd and rs is Integer    ==> No Change ...
  @ else                    ==> Fail
 *)
fun ckMulm (inf, debuginfo, tctx, env, i, rs, rd) = ckAddm (inf, debuginfo, tctx, env, i, rs, rd)

(*Movz i rd tp*)                                  (*-=DoNe=-*)
(*@ rd = ESP or EBP          ==> Fail
  @ PtrInfo wrong            ==> Fail
  @ rd is Int                ==> change according to i/tp (gmma pind)
  @ not leaking              ==> change gamma pind
 *)


(*Xchg rs rd*)                                   (*-=DoNe=-*)
(*@ rs or rd = ebp/esp        ==> Fail
  @ rs or rd is PTR           ==> Fail
 *)   
fun ckXchg (inf, debuginfo, tctx, env, rs, rd) =
    let val (pprop, PiP, PiSet, NSet, DSet, USet) = env
        val (asmenv, gamma) = tctx
        val tctx1 = (asmenv, gamma, debuginfo, env) 
        val pndu = (PiSet, NSet, DSet, USet)
        val (rsaptr, rdaptr) = (A.Preg(rs),A.Preg(rd))
        val (rsastr, rdastr) = (A.aptr2str(rsaptr),A.aptr2str(rdaptr))
        val (rstp, rdtp) = (getTypeAll (tctx1, rsaptr), getTypeAll (tctx1, rdaptr))
        val _ = outputInfo (tctx, env) (*Output Info*)
        val fail = fn str => setPosAndFail (debuginfo, tctx, env, str)
    in  if isRegStkreg2 (rs, rd)       (* rs rd = ESP or EBP => Fail*)
        then fail (rsastr^" or "^rdastr^" trying to exchange with esp/ebp...")
        else case (rstp, rdtp)
              of (A.Int, A.Int) => (*rs rd is Int => no change*)
                 (tctx, env)
               | (_ , A.Ptr(_)) => 
                 fail (rdastr^" try to exchange with ptr...not allowed...")
               | (A.Ptr(_), _) =>
                 fail (rsastr^" try to exchange with ptr...not allowed...")
               | (_, _) =>
                 fail (" non-integer type exchange... not allowed")                
    end

(*Movz i rd*)

fun ckMovz (inf, debuginfo, tctx, env, tp, i, rd) =
    let val (pprop, PiP, PiSet, NSet, DSet, USet) = env
        val (asmenv, gamma) = tctx
        val tctx1 = (asmenv, gamma, debuginfo, env) 
        val pndu = (PiSet, NSet, DSet, USet)
        val aptr = A.Preg(rd)
        val astr = A.aptr2str(aptr)
        val atp = getTypeAll (tctx1, aptr)
        val _ = outputInfo (tctx, env) (*Output Info*)
        val fail = fn str => setPosAndFail (debuginfo, tctx, env, str)
        val newtctx = (asmenv, setTypeGamma (gamma, aptr, tp))
        fun chN n =
            case (i,tp)
             of (0, A.Ptr(_)) => n
              | (_, A.Ptr(_)) => fail (astr^" trying to mov a non-zero ptr...")
              | (_, A.Int) => n
              | (_, _) => fail (astr^" trying to mov z not ptr or int...")        
    in if (isRegStkreg rd) (* rd = ESP or EBP => Fail*)
       then fail (astr^" trying to mov i to esp/ebp ... not allowed")
       else case (tp, atp)
             of ( A.Int, A.Int) =>                                   (* rd is Int => change according to i/tp *)
                let val _ = debugPrint (astr^" is int and moving int to it ...\n")
                in (tctx, env)
                end
              | (A.Ptr(_), A.Int) =>
                let val _ = debugPrint (astr^" is int and moving ptr to it ...\n")
                    val newN  = chN NSet
                    val newNSet = addPtrN (aptr, newN)
                in (newtctx, (pprop, PiP, PiSet, newNSet, DSet, USet))
                end
              | (A.Int, A.Ptr(_)) =>
                if not (isPtrInfoCorrect (tctx1, pndu, aptr))
                then fail (astr^" ptr info not correct...bug...")
                else (case (getPtrSort (aptr, pndu))
                       of P =>
                          if not_leaking(aptr, PiSet) (* not leaking  => change gamma piset*)          
                          then let val (newPprop, newPiP, newPi, newN, newD, newU)
                                     = adjustEnvAliasSubst (env, aptr)
                                   val newPiSet = deletePtrPi (aptr, newPi)
                               in (newtctx, (newPprop, newPiP, newPiSet, newN, newD, newU))
                               end
                          else fail (astr^" is singleton ptr, cause  memory leak...")
                        | N =>
                          let val newNSet = deletePtrN (aptr, NSet)
                          in  (newtctx, (pprop, PiP, PiSet, newNSet, DSet, USet))
                          end
                        | D =>
                          let val newDSet = deletePtrD (aptr, DSet)
                          in (newtctx, (pprop, PiP, PiSet, NSet, newDSet, USet))
                          end
                        | U => 
                          let val newUSet = deletePtrU (aptr, USet)
                          in (newtctx, (pprop, PiP, PiSet, NSet, DSet, newUSet))
                          end)                                                            
              | (A.Ptr(t1), A.Ptr(t2)) =>
                  if i <> 0
                  then fail (" moving none-NULL ptr, not allowed...")
                  else if not (isPtrInfoCorrect (tctx1, pndu, aptr))
                       then fail (astr^" ptr info not correct...bug...")
                       else (case (getPtrSort (aptr, pndu))
                              of P =>  (* not leaking  => change gamma piset*) 
                                 if not_leaking (aptr, PiSet) 
                                 then let val (newPprop, newPiP, newPi, newN, newD, newU) 
                                            = adjustEnvAliasSubst (env, aptr)
                                          val newPiSet = deletePtrPi (aptr, newPi)
                                          val newNSet  = addPtrN (aptr, newN)
                                      in (newtctx, (newPprop, newPiP, newPiSet, newNSet, newD, newU))
                                      end
                                 else fail (astr^" is singleton ptr, cause  memory leak...")
                               | N => (newtctx, env)
                               | D =>
                                 let val newDSet = deletePtrD (aptr, DSet)
                                     val newNSet = addPtrN (aptr, NSet)
                                 in  (newtctx, (pprop, PiP, PiSet, newNSet, newDSet, USet))
                                 end
                               | U =>
                                 let val newUSet = deletePtrU (aptr, USet)
                                     val newNSet = addPtrN (aptr, NSet)
                                 in (newtctx, (pprop, PiP, PiSet, newNSet, DSet, newUSet))
                                 end)                       
              |(_ , _) => fail (" either int or ptr move...not allowed") 
    end

(*Movr rs rd*)                                  (*-=DoNe=-*)
(*@ rs rd is Int     ==> no change
  @
 *)
fun ckMovr (inf, debuginfo, tctx, env, rs, rd) =
    let val (pprop, PiP, PiSet, NSet, DSet, USet) = env
        val (asmenv, gamma) = tctx
        val tctx1 = (asmenv, gamma, debuginfo, env) 
        val pndu = (PiSet, NSet, DSet, USet)
        val (rsaptr, rdaptr) = (A.Preg(rs),A.Preg(rd))
        val (rsastr, rdastr) = (A.aptr2str(rsaptr),A.aptr2str(rdaptr))
        val (rstp, rdtp) = (getTypeAll (tctx1, rsaptr), getTypeAll (tctx1, rdaptr))
        val _ = outputInfo (tctx, env) (*Output Info*)
        val fail = fn str => setPosAndFail (debuginfo, tctx, env, str)
        val newtctx = (asmenv, setTypeGamma (gamma, rdaptr, rstp))
    in if rs = A.Esp andalso rd = A.Ebp            (*mov esp ebp   => argument change form *)
       then let val _ = debugPrint "mov esp ebp   => argument change form\n"
                val newenv = adjustEnvEsp2Ebp env
                val newgamma = adjustGammaEsp2Ebp gamma
            in ((asmenv, newgamma), newenv)
            end
       else if rs = A.Ebp andalso rd = A.Esp            (*mov ebp esp   => argument change form *)
            then let val _ = debugPrint "mov ebp esp   => argument change form\n"
                     val newenv = adjustEnvEbp2Esp env
                     val newgamma = adjustGammaEbp2Esp gamma
                 in ((asmenv, newgamma), newenv)
                 end
            else case (rstp, rdtp) (*rs rd is Int  => no change*)
                  of (A.Int, A.Int) => 
                     let val _ =  debugPrint "rs rd is Int  => no change\n"
                     in (tctx, env)
                     end 
                   | (A.Ptr(_),A.Int) => (*rs is PI Ptr rd is Int  => adjust gamma pi *)
                     if not (isPtrInfoCorrect (tctx1, pndu, rsaptr))
                     then fail (rsastr^" ptr info not correct...bug...")
                     else (case (getPtrSort (rsaptr, pndu))
                            of P =>
                               let val newPi = addPtrPi (rdaptr, rsaptr, PiSet)
                               in (newtctx, (pprop, PiP, newPi, NSet, DSet, USet))
                               end
                             | N =>
                               let val newNSet = addPtrN (rdaptr, NSet)
                               in (newtctx, (pprop, PiP, PiSet, newNSet, DSet, USet))
                               end
                             | D =>
                               fail (rsastr^" is ptr in D...not allowed...")
                             | U => 
                               let val newUSet = addPtrU (rdaptr, rsaptr, USet)
                               in (newtctx, (pprop, PiP, PiSet, NSet, DSet, newUSet))
                               end)         
                   | (A.Int, A.Ptr(_)) =>  (*rd is PI N Ptr rs is Int  => adjust gamma pi *)
                     if not (isPtrInfoCorrect (tctx1, pndu, rdaptr))
                     then fail (rsastr^" ptr info not correct...bug...")
                     else (case (getPtrSort (rdaptr, pndu))
                            of P =>
                               if  not_leaking(rdaptr, PiSet)
                               then let val (newPprop, newPiP, newPi, newN, newD, newU)
                                          = adjustEnvAliasSubst (env, rdaptr)
                                        val newPiSet = deletePtrPi(rdaptr, newPi)
                                    in (newtctx, (newPprop, newPiP, newPiSet, newN, newD, newU))
                                    end
                               else fail (rdastr^" is singleton ptr in pi... meomery leaking")
                             | N =>
                               let val newN = deletePtrN(rdaptr, NSet)
                               in (newtctx, (pprop, PiP, PiSet, newN, DSet, USet))
                               end
                             | D =>
                               let val newD = deletePtrD(rdaptr, DSet)
                               in (newtctx, (pprop, PiP, PiSet, NSet, newD, USet))
                               end
                             | U => 
                               let val newUSet = deletePtrU(rdaptr, USet)
                               in (newtctx, (pprop, PiP, PiSet, NSet, DSet, newUSet))
                               end) 
                   | (A.Ptr(tp1), A.Ptr(tp2)) =>(*rd and rs are Ptr => case type info, adjust gamma pi *)
                     if not (isPtrInfoCorrect2 (tctx1, pndu, rsaptr, rdaptr))
                     then fail (rsastr^" or "^rdastr^" ptr info not correct...bug...")
                     else (case (getPtrSort (rsaptr, pndu), getPtrSort (rdaptr, pndu))
                            of (P, P) =>
                               if is2PtrInPiSameSet(rsaptr, rdaptr, PiSet) (*same type ptr => no change*)
                               then (tctx, env)
                               else if not_leaking(rdaptr, PiSet)       (*different ptr type and not leaking*)
                               then let val newenv = adjustEnvNotLeaking (env, rsaptr, rdaptr)
                                    in (newtctx, newenv)
                                    end
                               else fail (rdastr^" is in singleton pi set...memory leak") (*leak*)
                             | (P, N) =>
                               let val newNSet = deletePtrN (rdaptr, NSet)
                                   val newPiSet = addPtrPi (rdaptr, rsaptr, PiSet)
                               in (newtctx, (pprop, PiP, newPiSet, newNSet, DSet, USet))
                               end
                             | (P, D) =>
                               let val newDSet = deletePtrD (rdaptr, DSet)
                                   val newPiSet = addPtrPi (rdaptr, rsaptr, PiSet)
                               in (newtctx, (pprop, PiP, newPiSet, NSet, newDSet, USet))
                               end
                             | (P, U) => (*???*)
                               let val newUSet = deletePtrU (rdaptr, USet)
                                   val newPiSet = addPtrPi (rdaptr, rsaptr, PiSet)
                               in (newtctx, (pprop, PiP, newPiSet, NSet, DSet, newUSet))
                               end
                             | (N, P) =>
                               if not_leaking(rdaptr, PiSet)  (*not leak*)
                               then let val (newPprop, newPiP, newPi, newN, newD, newU) 
                                          = adjustEnvAliasSubst (env, rdaptr)
                                        val newPiSet = deletePtrPi (rdaptr, newPi)
                                        val newNSet = addPtrN (rdaptr, newN) 
                                    in (newtctx, (newPprop,newPiP, newPiSet, newNSet, newD, newU))
                                    end
                               else fail (rdastr^" is in singleton pi set...memory leak") (*leak*)
                             | (N, N) =>
                               (newtctx, env)
                             | (N, D) =>
                               let val newDSet = deletePtrD (rdaptr, DSet)
                                   val newNSet = addPtrN (rdaptr, NSet)
                               in  (newtctx, (pprop, PiP, PiSet, newNSet, newDSet, USet))
                               end
                             | (N, U) =>
                               let val newUSet = deletePtrU (rdaptr, USet)
                                   val newNSet = addPtrN (rdaptr, NSet)
                               in  (newtctx, (pprop, PiP, PiSet, newNSet, DSet, newUSet))
                               end
                             | (D, _) => 
                               fail (rsastr^" is in D Set...not allowed")
                             | (U, P) =>
                               if not_leaking(rdaptr, PiSet)  (*not leak*)
                               then let val (newPprop, newPiP, newPi, newN, newD, newU) 
                                          = adjustEnvAliasSubst (env, rdaptr)
                                        val newPiSet = deletePtrPi (rdaptr, newPi)
                                        val newUSet = addPtrU (rdaptr, rsaptr, newU) 
                                    in (newtctx, (newPprop,newPiP, newPiSet, newN, newD, newUSet))
                                    end
                               else fail (rdastr^" is in singleton pi set...memory leak") (*leak*)
                             | (U, N) =>
                               let val newNSet = deletePtrN (rdaptr, NSet)
                                   val newUSet = addPtrU (rdaptr, rsaptr, USet)
                               in (newtctx, (pprop, PiP, PiSet, newNSet, DSet, newUSet))
                               end
                             | (U, D) =>
                               let val newDSet = deletePtrD (rdaptr, DSet)
                                   val newUSet = addPtrU (rdaptr, rsaptr, USet)
                               in (newtctx, (pprop, PiP, PiSet, NSet, newDSet, newUSet))
                               end
                             | (U, U) =>
                               if is2PtrInUSameSet(rsaptr, rdaptr, USet) (*same type ptr => no change*)
                               then (tctx, env)
                               else let val u1 = deletePtrU (rdaptr, USet)
                                        val u2 = addPtrU (rdaptr, rsaptr, u1)
                                    in (newtctx, (pprop, PiP, PiSet, NSet, DSet, u2))
                                    end)
                   | (_,_) => fail ("not integer nor ptr mov... not allowed ")
    end

(*movst rs i(rd)*)                                  (*-=DoNe=-*)
(*@ rs i(rd) is Int     ==> no change
  @
 *)
fun ckMovst (inf, debuginfo, tctx, env, rs, i, rd) =
    let val (pprop, PiP, PiSet, NSet, DSet, USet) = env
        val (asmenv, gamma) = tctx
        val tctx1 = (asmenv, gamma, debuginfo, env) 
        val pndu = (PiSet, NSet, DSet, USet)
        val (rsaptr, rdaptr) = (A.Preg(rs), A.Pstk(i, rd))
        val (rsastr, rdastr) = (A.aptr2str(rsaptr),A.aptr2str(rdaptr))
        val (rstp, rdtp) = (getTypeAll (tctx1, rsaptr), getTypeAll (tctx1, rdaptr))
        val _ = outputInfo (tctx, env) (*Output Info*)
        val fail = fn str => setPosAndFail (debuginfo, tctx, env, str)
        val newtctx = (asmenv, setTypeGamma (gamma, rdaptr, rstp))
    in if rstp = rdtp orelse isRegEsp rd
       then let val _ = debugPrint "type equal or rd = esp \n"
            in case (rstp, rdtp)
                of (A.Int, A.Int) => (*rs rd are int => no change*)
                   let val _ = debugPrint "store int to int \n"
                   in (tctx, env)
                   end
                 | (A.Int, A.Ptr(_)) => (*rd = esp*)(*rd = esp, type can be changed*)
                   let val _ = debugPrint "store int to ptr \n"
                   in if not (isPtrInfoCorrect (tctx1, pndu, rdaptr))
                      then fail (rdastr^" ptr info not correct...bug...")
                      else (case (getPtrSort (rdaptr, pndu))
                             of P =>
                                if not_leaking (rdaptr, PiSet) (*not leaking*)
                                then let val _ = debugPrint (rdastr^" is not in singleton Pi Set \n")
                                         val (newPprop, newPiP, newPi, newN, newD, newU) = 
                                             adjustEnvAliasSubst (env, rdaptr)
                                         val newPiSet = deletePtrPi (rdaptr, newPi)
                                        
                                     in (newtctx, (newPprop,newPiP, newPiSet, newN, newD, newU))
                                     end
                                else fail (rdastr^" is in singleton Pi Set...memory leak") (*leak*)
                              | N =>
                                let val _ = debugPrint (rdastr^" is in N Set \n")
                                    val newNSet = deletePtrN (rdaptr, NSet)
                                in (newtctx, (pprop, PiP, PiSet, newNSet, DSet, USet))
                                end
                              | D =>
                                let val _ = debugPrint (rdastr^" is in D Set \n")
                                    val newDSet = deletePtrD (rdaptr, DSet)
                                in (newtctx, (pprop, PiP, PiSet, NSet, newDSet, USet))
                                end                          
                              | U =>
                                let val _ = debugPrint (rdastr^" is in U Set \n")
                                    val newUSet = deletePtrU (rdaptr, USet)
                                in (newtctx, (pprop, PiP, PiSet, NSet, DSet, newUSet))
                                end)
                   end
                 | (A.Ptr(_), A.Int) => (*rd = esp*)(*rd = esp, type can be changed*)
                   let val _ = debugPrint "store ptr to int \n"
                   in if not (isPtrInfoCorrect (tctx1, pndu, rsaptr))
                      then fail (rsastr^" ptr info not correct...bug...")
                      else (case (getPtrSort (rsaptr, pndu))
                             of P =>
                                let val _ = debugPrint (rsastr^" in Pi Set")
                                    val newPiSet = addPtrPi (rdaptr, rsaptr, PiSet)
                                in (newtctx, (pprop, PiP, newPiSet, NSet, DSet, USet))
                                end
                              | N =>
                                let val _ = debugPrint (rsastr^" in N Set")
                                    val newNSet = addPtrN (rsaptr, NSet)
                                in (newtctx, (pprop, PiP, PiSet, newNSet, DSet, USet))
                                end
                              | D => 
                                let val _ = debugPrint (rsastr^" in D Set")
                                in fail (rsastr^" is a Dangling ptr...not allowed")
                                end
                              | U =>
                                let val _ = debugPrint (rsastr^" in U Set")
                                    val newUSet = addPtrU (rdaptr, rsaptr, USet)
                                in (newtctx, (pprop, PiP, PiSet, NSet, DSet, newUSet))
                                end)
                   end
                 | (A.Ptr(t1), A.Ptr(t2)) => 
                   let val _ = debugPrint "store ptr to ptr \n"
                   in if not (isPtrInfoCorrect2 (tctx1, pndu, rsaptr, rdaptr))
                      then fail (rsastr^" or "^rdastr^" ptr info not correct...bug...")
                      else (case (getPtrSort (rsaptr, pndu), getPtrSort (rdaptr, pndu))
                             of (P, P) =>
                                let val _ = debugPrint "both ptr in Pi Set \n"
                                in if is2PtrInPiSameSet(rsaptr, rdaptr, PiSet) (*same PI*)
                                   then if t1 = t2 
                                        then let val _ = debugPrint "both ptr in Same Pi Set and types are equal"
                                             in (tctx, env)
                                             end
                                        else fail ("differet type ptr in same pi set...bug")
                                   else if not_leaking(rdaptr, PiSet)       (*different pi set and not leaking*)
                                        then let val _ = debugPrint (rdastr^" is not in singleton pi set \n") 
                                                 val newenv = adjustEnvNotLeaking (env, rsaptr, rdaptr)
                                             in if t1 = t2
                                                then let val _ = debugPrint "type equal \n" 
                                                     in (tctx, newenv)
                                                     end
                                                else if isRegEsp rd 
                                                     then let val _ = debugPrint "rd = esp \n" 
                                                          in (newtctx, newenv)
                                                          end
                                                     else fail ("differet type ptr moving ...not allowed") 
                                             end
                                        else fail (rdastr^" is leaking...memory leak") (*leak*)
                                end
                              | (P, N) =>
                                let val _ = debugPrint (rsastr^" is in Pi Set ;"^rdastr^" in N Set \n")
                                    val newNSet = deletePtrN (rdaptr, NSet)
                                    val newPiSet = addPtrPi (rdaptr, rsaptr, PiSet)
                                in (newtctx, (pprop, PiP, newPiSet, newNSet, DSet, USet))
                                end
                              | (P, D) =>
                                let val _ = debugPrint (rsastr^" is in Pi Set ;"^rdastr^" in D Set \n")
                                    val newDSet = deletePtrD (rdaptr, DSet)
                                    val newPiSet = addPtrPi (rdaptr, rsaptr, PiSet)
                                in (newtctx, (pprop, PiP, newPiSet, NSet, newDSet, USet))
                                end
                              | (P, U) =>
                                let val _ = debugPrint (rsastr^" is in Pi Set ;"^rdastr^" in U Set \n")
                                    val newUSet = deletePtrU (rdaptr, USet)
                                    val newPiSet = addPtrPi (rdaptr, rsaptr, PiSet)
                                in (newtctx, (pprop, PiP, newPiSet, NSet, DSet, newUSet))
                                end
                              | (N, P) =>
                                let val _ = debugPrint (rsastr^" is in N Set ;"^rdastr^" in P Set \n")
                                in if not_leaking(rdaptr, PiSet)  (*not leak*)
                                   then let val _ = debugPrint (rdastr^" is not in singleton Pi Set\n")
                                            val (newPprop, newPiP, newPi, newN, newD, newU) 
                                              = adjustEnvAliasSubst (env, rdaptr)
                                            val newPiSet = deletePtrPi (rdaptr, newPi)
                                            val newNSet = addPtrN (rdaptr, NSet)
                                        in (newtctx, (newPprop,newPiP, newPiSet, newNSet, newD, newU))
                                        end
                                   else fail (rdastr^" is in singleton pi set...memory leak") (*leak*)
                                end
                              | (N, N) =>
                                let val _ = debugPrint (rsastr^" is in N Set ;"^rdastr^" in N Set \n")
                                in (newtctx, env)
                                end
                              | (N, D) =>
                                let val _ = debugPrint (rsastr^" is in N Set ;"^rdastr^" in D Set \n")
                                    val newDSet = deletePtrD (rdaptr, DSet)
                                    val newNSet = addPtrN (rdaptr, NSet)
                                in  (newtctx, (pprop, PiP, PiSet, newNSet, newDSet, USet))
                                end
                              | (N, U) =>
                                let val _ = debugPrint (rsastr^" is in N Set ;"^rdastr^" in U Set \n")
                                    val newUSet = deletePtrU (rdaptr, USet)
                                    val newNSet = addPtrN (rdaptr, NSet)
                                in  (newtctx, (pprop, PiP, PiSet, newNSet, DSet, newUSet))
                                end
                              | (D, _) =>
                                let val _ = debugPrint (rsastr^" is in D Set ")
                                in fail (rsastr^" is in U set...not allowed")
                                end
                              | (U, P) =>
                                let val _ = debugPrint (rsastr^" is in U Set ;"^rdastr^" in Pi Set \n")
                                in if not_leaking(rdaptr, PiSet)  (*not leak*)
                                   then let val _ = debugPrint (rdastr^" is not in singleton Pi Set\n")
                                            val (newPprop, newPiP, newPi, newN, newD, newU) 
                                              = adjustEnvAliasSubst (env, rdaptr)
                                            val newPiSet = deletePtrPi (rdaptr, newPi)
                                            val newUSet = addPtrU (rdaptr,rsaptr, USet)
                                        in (newtctx, (newPprop,newPiP, newPiSet, newN, newD, newUSet))
                                        end
                                   else fail (rdastr^" is in singleton pi set...memory leak") (*leak*)
                                end
                              | (U, N) =>
                                let val _ = debugPrint (rsastr^" is in U Set ;"^rdastr^" in N Set \n")
                                    val newNSet = deletePtrN (rdaptr, NSet)
                                    val newUSet = addPtrU (rdaptr, rsaptr, USet)
                                in (newtctx, (pprop, PiP, PiSet, newNSet, DSet, newUSet))
                                end
                              | (U, D) =>
                                let val _ = debugPrint (rsastr^" is in U Set ;"^rdastr^" in D Set \n")
                                    val newDSet = deletePtrD (rdaptr, DSet)
                                    val newUSet = addPtrU (rdaptr, rsaptr, USet)
                                in  (newtctx, (pprop, PiP, PiSet, NSet, newDSet, newUSet))
                                end
                              | (U, U) =>
                                let val _ = debugPrint (rsastr^" is in U Set ;"^rdastr^" in U Set \n")
                                    val u1 = deletePtrU (rdaptr, USet)
                                    val newUSet = addPtrU (rdaptr, rsaptr, u1)
                                in  (newtctx, (pprop, PiP, PiSet, NSet, DSet, newUSet))
                                end)          
                   end
                 | (_ ,_) => fail ("not ptr or not int moving...bug")
            end
       else fail ("types are not equal or rd is not ESP ")
    end

fun outputFlist flist =
    case flist
     of [] => debugPrint ("\n")
      | (off, tp)::flist1 =>
         let val _ = debugPrint ("("^Int.toString(off)^", "^A.etype2str(tp)^")::")
         in outputFlist flist1
         end

fun addPtrFieldOne (gamma, uset, nset, reg, index, tp) =
    let val newaptr = A.Pstk(index, reg)
        val newg = setTypeGamma (gamma, newaptr, tp)
        val (newu, newn) = case tp
                            of A.Ptr(_) => 
                               if isPtrInN(newaptr, nset)
                               then (addSingletonU (newaptr, uset), deletePtrN (newaptr, nset))
                               else (addSingletonU (newaptr, uset), nset)
                             | _ => (uset, nset)
 
    in (newg, newu, newn)
    end

fun addPtrField (inf, tp, gamma, uset, nset, reg) =
    let fun loop (i, s, g, u, n, r, flist) = 
            let val len = List.length flist
            in if len >0  
               then let val (off, etp) = List.hd(flist) 
                        val _ = debugPrint ("("^Int.toString(off)^", "^A.etype2str(etp)^")\n")
                        val (ng, nu, nn) =  addPtrFieldOne (g, u, n, r, off, etp)
                    in loop (i, s, ng, nu, nn, r, List.tl(flist))
                    end
               else (g, u, n, 0)
            end
    in case tp
        of A.Str(str) =>
           let val sflist = A.getStrFields (str, inf)   
               val _ = debugPrint "Field List Debug.............\n"
               val _ = outputFlist sflist            
               val _ = debugPrint "..............................\n"
           in loop (inf, str, gamma, uset, nset, reg, sflist)
           end
         | _ => (gamma, uset, nset, 0)
    end
(*movld i(rs) rd*)
(*@ i(rs) rd is Int     ==> no change
  @
 *)
fun ckMovld (inf, debuginfo, tctx, env, i, rs, rd) =
    let val (pprop, PiP, PiSet, NSet, DSet, USet) = env
        val (asmenv, gamma) = tctx
        val tctx1 = (asmenv, gamma, debuginfo, env) 
        val pndu = (PiSet, NSet, DSet, USet)
        val (rsaptr, rdaptr) = (A.Pstk(i, rs), A.Preg(rd))
        val (rsastr, rdastr) = (A.aptr2str(rsaptr), A.aptr2str(rdaptr))
        val (rstp, rdtp) = (getTypeAll (tctx1, rsaptr), getTypeAll (tctx1, rdaptr))
        val fail = fn str => setPosAndFail (debuginfo, tctx, env, str)
        val newgamma = setTypeGamma (gamma, rdaptr, rstp)
        val newtctx = (asmenv, newgamma)
        val _ = outputInfo (tctx, env) (*Output Info*)
    in case (rstp, rdtp)
        of (A.Int, A.Int) =>  (*rs rd are int => no change*)
           let val _ = debugPrint "store int to int \n"
           in (tctx, env)
           end
         | (A.Int, A.Ptr(_)) =>
           let val  _ = debugPrint "load int to ptr \n"
           in if not (isPtrInfoCorrect (tctx1, pndu, rdaptr))
              then fail (rdastr^" ptr info not correct...bug...")
              else (case (getPtrSort (rdaptr, pndu))
                     of P =>
                        if not_leaking (rdaptr, PiSet) (*not leaking*)
                        then let val _ = debugPrint (rdastr^" is not in singleton Pi Set \n") 
                                 val (newPprop, newPiP, newPi, newN, newD , newU)
                                   = adjustEnvAliasSubst (env, rdaptr)
                                 val newPiSet = deletePtrPi (rdaptr, newPi)
                             in (newtctx, (newPprop,newPiP, newPiSet, newN, newD, newU))
                             end
                        else fail (rdastr^" is in singleton Pi Se...memory leak") (*leak*)
                      | N =>
                        let val _ = debugPrint (rdastr^" is in N Set \n")
                            val newNSet = deletePtrN (rdaptr, NSet)
                        in (newtctx, (pprop, PiP, PiSet, newNSet, DSet, USet))
                        end
                      | D =>
                        let val _ = debugPrint (rdastr^" is in D Set \n")
                            val newDSet = deletePtrD (rdaptr, DSet)
                        in (newtctx, (pprop, PiP, PiSet, NSet, newDSet, USet))
                        end
                      | U =>
                        let val _ = debugPrint (rdastr^" is in U Set \n")
                            val newUSet = deletePtrU (rdaptr, USet)
                        in (newtctx, (pprop, PiP, PiSet, NSet, DSet, newUSet))
                        end)          
           end
         | (A.Ptr(t), A.Int) =>
          let val _ = debugPrint "load ptr to int \n"
          in if not (isPtrInfoCorrect (tctx1, pndu, rsaptr))
             then fail (rsastr^" ptr info not correct...bug...")
             else (case (getPtrSort (rsaptr, pndu))
                    of P =>  
                       let val _ = debugPrint (rsastr^" in Pi Set\n")
                           val newPiSet = addPtrPi (rdaptr, rsaptr, PiSet)
                           val (newgamma2, newUSet, newNSet, _) = addPtrField (inf, t, newgamma, USet, NSet, rd)
                       in ((asmenv, newgamma2), (pprop, PiP, newPiSet, newNSet, DSet, newUSet))
                        end
                     | N =>
                       let val _ = debugPrint (rsastr^" in N Set\n")
                           val newNSet = addPtrN (rsaptr, NSet)
                       in (newtctx, (pprop, PiP, PiSet, newNSet, DSet, USet))
                       end
                     | D =>
                       let val _ = debugPrint (rsastr^" in D Set\n")
                       in fail (rsastr^" is a Dangling ptr...not allowed")
                       end
                     | U =>
                       let val _ = debugPrint (rsastr^" in U Set\n")
                           val newUSet = addPtrU (rdaptr, rsaptr, USet)
                       in (newtctx, (pprop, PiP, PiSet, NSet, DSet, newUSet))
                       end)  
          end
         | (A.Ptr(t1), A.Ptr(t2)) => 
           let val _ = debugPrint "load ptr to ptr \n"
           in if not (isPtrInfoCorrect2 (tctx1, pndu, rsaptr, rdaptr))
              then fail (rsastr^" or "^rdastr^" ptr info not correct...bug...")
              else (case (getPtrSort (rsaptr, pndu), getPtrSort (rdaptr, pndu))
                     of (P, P) =>
                        let val _ = debugPrint "both ptr in Pi Set \n"
                        in if is2PtrInPiSameSet(rsaptr, rdaptr, PiSet) (*same PI*)
                           then if t1 = t2 
                                then let val _ = debugPrint "both ptr in Same Pi Set and types are equal\n"
                                     in (tctx, env)
                                     end
                                else fail ("differet type ptr in same pi set...bug")
                           else if not_leaking(rdaptr, PiSet)       (*different pi set and not leaking*)
                                then let val _ = debugPrint (rdastr^" is not in singleton pi set \n") 
                                         val newenv = adjustEnvNotLeaking (env, rsaptr, rdaptr)
                                         val (npprop, npip, npiset, nnset, ndset, nuset) = newenv
                                         val (newgamma2, newUSet, newNSet,  _) = addPtrField (inf, t1, newgamma, nuset, nnset, rd)
                                     in if t1 = t2
                                        then let val _ = debugPrint "type equal \n" 
                                             in ((asmenv, newgamma2), (npprop, npip, npiset, newNSet, ndset, newUSet))
                                             end
                                        else let val _ = debugPrint "type different \n" 
                                             in ((asmenv, newgamma2), (npprop, npip, npiset, newNSet, ndset, newUSet))
                                             end
                                     end
                                else fail (rdastr^" is in singleton pi set...memory leak") (*leak*)
                        end
                      | (P, N) =>
                        let val _ = debugPrint (rsastr^" is in Pi Set ;"^rdastr^" in N Set \n")
                            val newNSet = deletePtrN (rdaptr, NSet)
                            val newPiSet = addPtrPi (rdaptr, rsaptr, PiSet)
                        in (newtctx, (pprop, PiP, newPiSet, newNSet, DSet, USet))
                        end
                      | (P, D) =>
                        let val _ = debugPrint (rsastr^" is in Pi Set ;"^rdastr^" in D Set \n")
                            val newDSet = deletePtrD (rdaptr, DSet)
                            val newPiSet = addPtrPi (rdaptr, rsaptr, PiSet)
                        in (newtctx, (pprop, PiP, newPiSet, NSet, newDSet, USet))
                        end
                      | (P, U) =>
                        let val _ = debugPrint (rsastr^" is in Pi Set ;"^rdastr^" in U Set \n")
                            val newUSet = deletePtrU (rdaptr, USet)
                            val newPiSet = addPtrPi (rdaptr, rsaptr, PiSet)
                        in (newtctx, (pprop, PiP, newPiSet, NSet, DSet, newUSet))
                        end
                      | (N, P) =>
                        let val _ = debugPrint (rsastr^" is in N Set ;"^rdastr^" in P Set \n")
                        in if not_leaking(rdaptr, PiSet)  (*not leak*)
                           then let val _ = debugPrint (rdastr^" is not in singleton Pi Set\n")
                                    val (newPprop, newPiP, newPi, newN, newD, newU) 
                                      = adjustEnvAliasSubst (env, rdaptr)
                                    val newPiSet = deletePtrPi (rdaptr, newPi)
                                    val newNSet = addPtrN (rdaptr, newN)
                                in (newtctx, (newPprop,newPiP, newPiSet, newNSet, newD, newU))
                                end
                           else fail (rdastr^" is in singleton pi set...memory leak") (*leak*)
                        end
                      | (N, N) =>
                        let val _ = debugPrint (rsastr^" is in N Set ;"^rdastr^" in N Set \n")
                        in (newtctx, env)
                        end
                      | (N, D) =>
                        let val _ = debugPrint (rsastr^" is in N Set ;"^rdastr^" in D Set \n")
                            val newDSet = deletePtrD (rdaptr, DSet)
                            val newNSet = addPtrN (rdaptr, NSet)
                        in  (newtctx, (pprop, PiP, PiSet, newNSet, newDSet, USet))
                        end
                      | (N, U) =>
                        let val _ = debugPrint (rsastr^" is in N Set ;"^rdastr^" in U Set \n")
                            val newUSet = deletePtrU (rdaptr, USet)
                            val newNSet = addPtrN (rdaptr, NSet)
                        in  (newtctx, (pprop, PiP, PiSet, newNSet, DSet, newUSet))
                        end
                      | (D, _) =>
                        let val _ = debugPrint (rsastr^" is in D Set ")
                        in fail (rsastr^" is in D set (Dangling Pointer Set)...not allowed")
                        end
                      | (U, P) =>
                        let val _ = debugPrint (rsastr^" is in U Set ;"^rdastr^" in Pi Set \n")
                        in if not_leaking(rdaptr, PiSet)  (*not leak*)
                           then let val _ = debugPrint (rdastr^" is not in singleton Pi Set\n")
                                    val newUSet = addPtrU (rdaptr,rsaptr, USet)
                                    val (newPprop, newPiP, newPi, newN, newD, newU) 
                                      = adjustEnvAliasSubst ((pprop, PiP, PiSet, NSet, DSet, newUSet), rdaptr)
                                    val newPiSet = deletePtrPi (rdaptr, newPi)
                                in (newtctx, (newPprop,newPiP, newPiSet, newN, newD, newUSet))
                                end
                           else fail (rdastr^" is in singleton pi set...memory leak") (*leak*)
                        end
                      | (U, N) =>
                        let val _ = debugPrint (rsastr^" is in U Set ;"^rdastr^" in N Set \n")
                            val newN = deletePtrN (rdaptr, NSet)
                            val newU = addPtrU (rdaptr, rsaptr, USet)
                        in (newtctx, (pprop, PiP, PiSet, newN, DSet, newU))
                        end
                      | (U, D) =>
                        let val _ = debugPrint (rsastr^" is in U Set ;"^rdastr^" in D Set \n")
                            val newDSet = deletePtrD (rdaptr, DSet)
                            val newUSet = addPtrU (rdaptr, rsaptr, USet)
                        in  (newtctx, (pprop, PiP, PiSet, NSet, newDSet, newUSet))
                        end
                      | (U, U) =>
                        let val _ = debugPrint (rsastr^" is in U Set ;"^rdastr^" in U Set \n")
                        in if is2PtrInUSameSet (rsaptr, rdaptr, USet)
                           then let val _ = debugPrint (rsastr^" and "^rdastr^" in same U Set\n")
                                in if t1 = t2
                                   then (tctx, env)
                                   else fail  (rsastr^" and "^rdastr^" in same U Set, but types are different\n")
                                end
                           else let val _ = debugPrint (rsastr^" and "^rdastr^" in different U Set\n")
                                    val u1 = deletePtrU (rdaptr, USet)
                                    val newUSet = addPtrU (rdaptr, rsaptr, u1)
                                in  (newtctx, (pprop, PiP, PiSet, NSet, DSet, newUSet))
                                end
                        end)
           end
         | (_ ,_) => fail ("not ptr or not int load...bug")
    end

(*push rs*)                                  (*-=DoNe=-*)
(*@ push ebp esp or Int(rs) ==> adjust gamma env
  @ PtrInfo wrong           ==> Fail
  @ rs is PTR in pi         ==> adjust gamma pi
  @ rs is PTR in n d        ==> Fail
  @ else                    ==> Fail
 *)   
fun ckPush (inf, debuginfo, tctx, env, rs) =
    let val (pprop, PiP, PiSet, NSet, DSet, USet) = env
        val (asmenv, gamma) = tctx
        val tctx1 = (asmenv, gamma, debuginfo, env) 
        val pndu = (PiSet, NSet, DSet, USet)
        val aptr = A.Preg(rs)
        val astr = A.aptr2str(aptr)
        val atp  = getTypeAll (tctx1, aptr)
        val tctx1 = (asmenv, gamma, debuginfo, env) 
        val newgamma = setTypeGamma (adjustGamma (gamma, (A.Preg(A.Esp)), (~4)), A.Pstk(0, A.Esp), atp)
        val (nPprop, nPiP, nPiSet, nNSet, nDSet, nUSet) = adjustEnv (env, (A.Preg(A.Esp)), (~4))
        val newtctx = (asmenv, newgamma)
        val _ = outputInfo (tctx, env) (*Output Info*) 
        val fail = fn str => setPosAndFail (debuginfo, tctx, env, str)
    in case atp
        of A.Int => (* push ebp esp or Int(rs) => adjust gamma env*)
           let val _ = debugPrint (astr^"'s type is int \n ")
           in (newtctx, adjustEnv (env, (A.Preg(A.Esp)),(~4))) 
           end
         | A.Ptr(_) => (* PtrInfo wrong => Fail *)   
           let val _ = debugPrint (astr^"'s type is ptr \n ")
           in if not (isPtrInfoCorrect (tctx1, pndu, aptr))                          
              then fail (astr^" not in pi n d u , but is Ptr...\n")
              else (case getPtrSort(aptr, pndu)
                     of P =>(* rs is PTR => adjust gamma pi *)
                        let val _ = debugPrint (astr^" is ptr in Pi Set \n ")
                            val newPiSet = addPtrPi(A.Pstk(0,A.Esp), aptr, nPiSet)
                        in (newtctx, (nPprop, nPiP, newPiSet, nNSet, nDSet, nUSet))
                        end                     
                      | N =>(*rs is PTR in n => adjust gamma N*)
                        let val _ = debugPrint (astr^" is ptr in N Set \n ")
                            val newNSet = addPtrN (A.Pstk(0,A.Esp), nNSet)
                        in (newtctx, (nPprop, nPiP, nPiSet, newNSet, nDSet, nUSet))
                        end
                      | D =>(*rs is PTR in d => Fail*)
                        let val _ = debugPrint (astr^" is ptr in D Set \n ")
                        in fail (A.aptr2str(aptr)^" in D Set...not allowed...\n")
                        end
                      | U =>(*rs is PTR in u => adjust gamma U*) (*argument case*)
                        let val _ = debugPrint (astr^" is ptr in U Set \n ")
                            val newUSet = addPtrU(A.Pstk(0,A.Esp), aptr, nUSet)
                        in (newtctx, (nPprop, nPiP, nPiSet, nNSet, nDSet, newUSet))
                        end)
           end
         | _ => fail ("try to push a reg not int or ptr")
    end

(*pop rd*)
fun ckPop (inf, debuginfo, tctx, env, rd) =
    let val (pprop, PiP, PiSet, NSet, DSet, USet) = env
        val pndu = (PiSet, NSet, DSet, USet)
        val (asmenv, gamma) = tctx
        val tctx1 = (asmenv, gamma, debuginfo, env) 
        val (stkaptr, rdaptr) = (A.Pstk(0, A.Esp), A.Preg(rd))
        val (stkastr, rdastr) = (A.aptr2str(stkaptr), A.aptr2str(rdaptr))
        val (stktp, rdtp)  = (getTypeAll (tctx1, stkaptr), getTypeAll (tctx1, rdaptr))        
        val newgamma = setTypeGamma (adjustGamma (gamma, (A.Preg(A.Esp)), 4), rdaptr, stktp)
        val newtctx = (asmenv, newgamma)
        val _ = outputInfo (tctx, env) (*Output Info*) 
        val fail = fn str => setPosAndFail (debuginfo, tctx, env, str)
    in if isRegEsp rd 
       then fail ("pop to "^rdastr^" not allowed \n ")
       else if isRegEbp rd 
            then if stktp = A.Int andalso rdtp = A.Int
                 then (newtctx, adjustEnv (env, (A.Preg(A.Esp)),4))
                 else fail (" can only pop int to ebp, ebp must be int type ...")
            else case (stktp, rdtp)
                  of (A.Int, A.Int) =>
                     let val _ = debugPrint (stkastr^" and "^rdastr^" are all int type  \n ")
                     in (newtctx, adjustEnv (env, (A.Preg(A.Esp)),4)) 
                     end
                   | (A.Ptr(_), A.Int) =>
                     let val _ = debugPrint (stkastr^" is ptr, "^rdastr^" is int   \n ")
                     in  if not (isPtrInfoCorrect (tctx1, pndu, stkaptr))                          
                         then fail (stkastr^" is not in pi n d u, but is Ptr...\n")
                         else (case getPtrSort(stkaptr, pndu)
                                of P =>(* 0(esp) is PTR => adjust gamma pi *)
                                   let val _ = debugPrint (stkastr^" is ptr in Pi Set \n ")
                                       val env1 = adjustEnvSubstAndDeletePi (env, stkaptr, rdaptr)
                                       val newenv  = adjustEnv (env1, (A.Preg(A.Esp)), 4)
                                   in (newtctx, newenv)
                                   end         
                                 | N =>(*0(esp) is PTR in n => adjust gamma N*)
                                   let val _ = debugPrint (stkastr^" is ptr in N Set \n ")
                                       val n1 = deletePtrN (stkaptr, NSet)
                                       val n2 = addPtrN (rdaptr, n1)
                                       val env1 = (pprop, PiP, PiSet, n2, DSet, USet)
                                       val newenv = adjustEnv (env1, (A.Preg(A.Esp)), 4)
                                   in (newtctx, newenv)
                                   end
                                 | D =>(*0(esp) is PTR in d => Fail*)
                                   let val _ = debugPrint (stkastr^" is ptr in D Set \n ")
                                   in fail (stkastr^" in D Set...not allowed...bug...\n")
                                   end
                                 | U =>(*0(esp) is PTR in u => adjust gamma U*) (*argument case*)
                                   let val _ = debugPrint (stkastr^" is ptr in U Set \n ")
                                       val env1 = adjustEnvSubstAndDeleteU (env, stkaptr, rdaptr)
                                       val newenv  = adjustEnv (env1, (A.Preg(A.Esp)), 4)
                                   in (newtctx, newenv)
                                   end)
                     end
                   | (A.Int, A.Ptr(_)) =>
                     let val _ = debugPrint (stkastr^" is int, "^rdastr^" is ptr   \n ")
                     in  if not (isPtrInfoCorrect (tctx1, pndu, rdaptr))                          
                         then fail (rdastr^" is not in pi n d u, but is Ptr...\n")
                         else (case getPtrSort(rdaptr, pndu)
                                of P =>(* rd is PTR => adjust gamma pi *)
                                   let val _ = debugPrint (rdastr^" is ptr in Pi Set \n ")
                                   in if not_leaking (rdaptr, PiSet)
                                      then let val _ = debugPrint (rdastr^" is not in singleton Pi Set \n ")
                                               val pi1 = deletePtrPi (rdaptr, PiSet)
                                               val env1  = (pprop, PiP, pi1, NSet, DSet, USet)
                                               val newenv  = adjustEnv (env1, (A.Preg(A.Esp)), 4)
                                           in (newtctx, newenv)
                                           end
                                      else fail (rdastr^" is in singleton Pi Set... memory leaking \n ")
                                   end         
                                 | N =>(*rd is PTR in n => adjust gamma N*)
                                   let val _ = debugPrint (rdastr^" is ptr in N Set \n ")
                                       val n1 = deletePtrN (rdaptr, NSet)
                                       val env1 = (pprop, PiP, PiSet, n1, DSet, USet)
                                       val newenv = adjustEnv (env1, (A.Preg(A.Esp)), 4)
                                   in (newtctx, newenv)
                                   end
                                 | D =>(*rd is PTR in d => Fail*)
                                   let val _ = debugPrint (rdastr^" is ptr in D Set \n ")
                                       val d1 = deletePtrD (rdaptr, DSet)
                                       val env1 = (pprop, PiP, PiSet, NSet, d1, USet)
                                       val newenv = adjustEnv (env1, (A.Preg(A.Esp)), 4)
                                   in (newtctx, newenv)
                                   end
                                 | U =>(*rd is PTR in u => adjust gamma U*) (*argument case*)
                                   let val _ = debugPrint (rdastr^" is not in singleton Pi Set \n ")
                                       val u1 = deletePtrU (rdaptr, USet)
                                       val env1  = (pprop, PiP, PiSet, NSet, DSet, u1)
                                       val newenv  = adjustEnv (env1, (A.Preg(A.Esp)), 4)
                                   in (newtctx, newenv)
                                   end)
                     end
                   | (A.Ptr(t1), A.Ptr(t2)) =>
                     let val _ = debugPrint (stkastr^" is ptr, "^rdastr^" is ptr   \n ")
                         val rsaptr = stkaptr
                         val rsastr = stkastr
                         val rstp = stktp
                     in  if not (isPtrInfoCorrect2 (tctx1, pndu, rsaptr, rdaptr))                          
                         then fail (rsastr^" is ptr, "^rdastr^" is ptr, but one or both not in pi n d u...\n")
                         else (case (getPtrSort(rsaptr, pndu), getPtrSort(rdaptr, pndu))
                                of (P, P) =>
                                   let val _ = debugPrint "both ptr in Pi Set \n"
                                   in if is2PtrInPiSameSet(rsaptr, rdaptr, PiSet) (*same PI*)
                                      then if t1 = t2 
                                           then let val _ = debugPrint "both ptr in Same Pi Set and types are equal"
                                                    val _ = debugPrint (rdastr^" is not in singleton Pi Set \n ")
                                                    val env1 = adjustEnvSubstAndDeletePi (env, rsaptr, rdaptr)
                                                    val newenv  = adjustEnv (env1, (A.Preg(A.Esp)), 4)
                                                in (newtctx, newenv)
                                                end
                                           else fail ("differet type ptr in same pi set...bug")
                                      else if not_leaking(rdaptr, PiSet)       (*different pi set and not leaking*)
                                           then let val _ = debugPrint (rdastr^" is not in singleton pi set \n") 
                                                    val env1 = adjustEvnNotLeakingSubstAndDeleteRsPi (env, rsaptr, rdaptr)
                                                    val newenv  = adjustEnv (env1, (A.Preg(A.Esp)), 4)
                                                in (newtctx, newenv)
                                                end
                                           else fail (rdastr^" is in singleton pi set...memory leak") (*leak*)
                                   end
                                 | (P, N) =>
                                   let val _ = debugPrint (rsastr^" is in Pi Set ;"^rdastr^" in N Set \n")
                                       val newNSet = deletePtrN (rdaptr, NSet)
                                       val newPiSet = addPtrPi (rdaptr, rsaptr, PiSet)
                                       val env0 = (pprop, PiP, newPiSet, newNSet, DSet, USet)
                                       val env1 = adjustEnvSubstAndDeletePi (env0, rsaptr, rdaptr)
                                       val newenv  = adjustEnv (env1, (A.Preg(A.Esp)), 4)
                                   in (newtctx, newenv)
                                   end
                                 | (P, D) =>
                                   let val _ = debugPrint (rsastr^" is in Pi Set ;"^rdastr^" in D Set \n")
                                       val newDSet = deletePtrD (rdaptr, DSet)
                                       val newPiSet = addPtrPi (rdaptr, rsaptr, PiSet)
                                       val env0 = (pprop, PiP, newPiSet, NSet, newDSet, USet)
                                       val env1 = adjustEnvSubstAndDeletePi (env0, rsaptr, rdaptr)
                                       val newenv  = adjustEnv (env1, (A.Preg(A.Esp)), 4)
                                   in (newtctx, newenv)
                                   end
                                 | (P, U) =>
                                   let val _ = debugPrint (rsastr^" is in Pi Set ;"^rdastr^" in U Set \n")
                                       val newUSet = deletePtrU (rdaptr, USet)
                                       val newPiSet = addPtrPi (rdaptr, rsaptr, PiSet)
                                       val env0 = (pprop, PiP, newPiSet, NSet, DSet, newUSet)
                                       val env1 = adjustEnvSubstAndDeletePi (env0, rsaptr, rdaptr)
                                       val newenv  = adjustEnv (env1, (A.Preg(A.Esp)), 4)
                                   in (newtctx, newenv)
                                   end
                                 | (N, P) =>
                                   let val _ = debugPrint (rsastr^" is in N Set ;"^rdastr^" in P Set \n")
                                   in if not_leaking(rdaptr, PiSet)  (*not leak*)
                                      then let val _ = debugPrint (rdastr^" is not in singleton Pi Set\n")
                                               val (newPprop, newPiP, newPi, newN, newD, newU) 
                                                 = adjustEnvAliasSubst (env, rdaptr)
                                               val newPiSet = deletePtrPi (rdaptr, newPi)
                                               val n1 = deletePtrN (rsaptr, newN)
                                               val newNSet = addPtrN (rdaptr, n1)
                                               val env1 = (pprop, PiP, newPiSet, newNSet, DSet, USet)
                                               val newenv  = adjustEnv (env1, (A.Preg(A.Esp)), 4)
                                           in (newtctx, newenv)
                                           end
                                      else fail (rdastr^" is in singleton pi set...memory leak") (*leak*)
                                   end
                                 | (N, N) =>
                                   let val _ = debugPrint (rsastr^" is in N Set ;"^rdastr^" in N Set \n")
                                       val n1 = deletePtrN (rsaptr, NSet)
                                       val env1 = (pprop, PiP, PiSet, n1, DSet, USet)
                                       val newenv  = adjustEnv (env1, (A.Preg(A.Esp)), 4)
                                   in (newtctx, newenv)
                                   end
                                 | (N, D) =>
                                   let val _ = debugPrint (rsastr^" is in N Set ;"^rdastr^" in D Set \n")
                                       val n1 = deletePtrN (rsaptr, NSet)
                                       val newDSet = deletePtrD (rdaptr, DSet)
                                       val newNSet = addPtrN (rdaptr, n1)
                                       val env1 = (pprop, PiP, PiSet, newNSet, newDSet, USet)
                                       val newenv  = adjustEnv (env1, (A.Preg(A.Esp)), 4)
                                   in  (newtctx, newenv)
                                   end
                                 | (N, U) =>
                                   let val _ = debugPrint (rsastr^" is in N Set ;"^rdastr^" in U Set \n")
                                       val n1 = deletePtrN (rsaptr, NSet)               
                                       val newUSet = deletePtrU (rdaptr, USet)
                                       val newNSet = addPtrN (rdaptr, n1)
                                       val env1 = (pprop, PiP, PiSet, newNSet, DSet, newUSet)
                                       val newenv  = adjustEnv (env1, (A.Preg(A.Esp)), 4)
                                   in  (newtctx, newenv)
                                   end
                                 | (D, _) =>
                                   let val _ = debugPrint (rsastr^" is in D Set ")
                                   in fail (rsastr^" is in U set...not allowed")
                                   end
                                 | (U, P) =>
                                   let val _ = debugPrint (rsastr^" is in U Set ;"^rdastr^" in Pi Set \n")
                                   in if not_leaking(rdaptr, PiSet)  (*not leak*)
                                      then let val _ = debugPrint (rdastr^" is not in singleton Pi Set\n")
                                               val (newPprop, newPiP, newPi, newN, newD, newU) 
                                                 = adjustEnvAliasSubst (env, rdaptr)
                                               val newPiSet = deletePtrPi (rdaptr, newPi)
                                               val u1 = addPtrU (rdaptr,rsaptr, USet)
                                               val newUSet = deletePtrU (rsaptr, u1)
                                               val env1 = (pprop, PiP, newPiSet, NSet, DSet, newUSet)
                                               val newenv  = adjustEnv (env1, (A.Preg(A.Esp)), 4)
                                           in (newtctx, newenv)
                                           end
                                      else fail (rdastr^" is in singleton pi set...memory leak") (*leak*)
                                   end
                                 | (U, N) =>
                                   let val _ = debugPrint (rsastr^" is in U Set ;"^rdastr^" in N Set \n")
                                       val newNSet = deletePtrN (rdaptr, NSet)
                                       val u1 = addPtrU (rdaptr,rsaptr, USet)
                                       val newUSet = deletePtrU (rsaptr, u1)
                                       val env1 = (pprop, PiP, PiSet, newNSet, DSet, newUSet)
                                       val newenv  = adjustEnv (env1, (A.Preg(A.Esp)), 4)
                                   in (newtctx, newenv)
                                   end
                                 | (U, D) =>
                                   let val _ = debugPrint (rsastr^" is in U Set ;"^rdastr^" in D Set \n")
                                       val newDSet = deletePtrD (rdaptr, DSet)
                                       val u1 = addPtrU (rdaptr, rsaptr, USet)
                                       val newUSet = deletePtrU (rsaptr, u1)
                                       val env1 = (pprop, PiP, PiSet, NSet, newDSet, newUSet)
                                       val newenv  = adjustEnv (env1, (A.Preg(A.Esp)), 4)
                                   in (newtctx, newenv)
                                   end
                                 | (U, U) =>
                                   let val _ = debugPrint (rsastr^" is in U Set ;"^rdastr^" in U Set \n")
                                       val u1 = addPtrU (rdaptr, rsaptr, USet)
                                       val newUSet = deletePtrU (rsaptr, u1)
                                       val env1 = (pprop, PiP, PiSet, NSet, DSet, newUSet)
                                       val newenv  = adjustEnv (env1, (A.Preg(A.Esp)), 4)
                                   in (newtctx, newenv)
                                   end)
                     end
                   | _ => fail ("try to pop non-int nor ptr data .... bug")                    
    end

(*free rs*)
fun ckFree (inf, debuginfo, tctx, env, rs) =
    let val (pprop, PiP, PiSet, NSet, DSet, USet) = env
        val pndu = (PiSet, NSet, DSet, USet)
        val (asmenv, gamma) = tctx
        val tctx1 = (asmenv, gamma, debuginfo, env) 
        val rdaptr = A.Preg(rs)
        val rdastr = A.aptr2str(rdaptr)
        val rdtp   = getTypeAll (tctx1, rdaptr)
        val newgamma = gamma(*setTypeGamma (gamma, rdaptr, A.Int)*)
        val newtctx = (asmenv, newgamma)
        val _ = outputInfo (tctx, env) (*Output Info*) 
        val fail = fn str => setPosAndFail (debuginfo, tctx, env, str)
    in case rdtp
        of A.Int => fail "Bug: try to free a int register...\n"
         | A.Ptr(tp) =>
           (case (getPtrSort(rdaptr, pndu))
             of P =>
                let val _ = debugPrint "Free a Effective ptr..\n"
                    val rdset = set2elem (getPtrSet (rdaptr, PiSet))
                    val newPiSet = deleteSetPi (rdset, PiSet)
                    val newNSet = deleteNDBase (rdaptr, NSet)
                    val newDSet1 = deleteNDBase (rdaptr, DSet)
                    val newDSet = NDSet.addList(newDSet1, toList rdset)
                    fun deleteU (list, u) =
                        case list
                         of [] => u
                          | x::xs=>
                            let val u1 = deleteU (xs, u)
                            in deleteUBase (x, u1)
                            end
                    fun deleteGM (list, g) =
                        case list
                         of [] => g
                          | x::xs=>
                            let val g1 = deleteGM (xs, g)
                            in deleteAptrBaseInGamma (g1, x)
                            end
                    val newUSet = deleteU (toList rdset, USet)
                    val newGM = deleteGM (toList rdset, gamma)                                  
                in ((asmenv, newGM), (pprop, PiP, newPiSet, newNSet, newDSet, newUSet))
                end 
              | N =>
                let val _ = debugPrint "Free a NULL ptr..\n"
                in fail "Try to free NULL pointer"
                end 
              | D => 
                let val _ = debugPrint "Free a Dangling ptr..\n"
                in fail "Try to free Dangling pointer"
                end
              | U =>
                let val _ = debugPrint "Free a Unknown ptr..\n"
                in fail "Try to free Unknown pointer"
                end)          
         | _ => fail "Bug: try to free a non-ptr register...\n"
    end

fun ckInstr (inf, debuginfo, tctx, env, cblks, instr) =
    let val _ = debugPrint ("\n\nNow checking instruction : "^(A.toString instr)^" \n\n")
        val t = (tctx, env)
        val fail = fn str => setPosAndFail (debuginfo, tctx, env, str)
        val debuginfo = setDebugInstr (debuginfo, instr)
    in  case instr
         of A.Addr(rs, rd)    => ckAddr (inf, debuginfo, tctx, env, rs, rd)
          | A.Addz(i, rd)     => ckAddz (inf, debuginfo, tctx, env, i,  rd)
          | A.Addm(i, rs, rd) => ckAddm (inf, debuginfo, tctx, env, i, rs, rd)
          | A.Subr(rs, rd)    => ckSubr (inf, debuginfo, tctx, env, rs, rd)
          | A.Subz(i, rd)     => ckSubz (inf, debuginfo, tctx, env, i,  rd)
          | A.Subm(i, rs, rd) => ckSubm (inf, debuginfo, tctx, env, i, rs, rd)
          | A.Mulr(rs, rd)    => ckMulr (inf, debuginfo, tctx, env, rs, rd)
          | A.Mulz(i, rd)     => ckMulz (inf, debuginfo, tctx, env, i,  rd)
          | A.Mulm(i, rs, rd) => ckMulm (inf, debuginfo, tctx, env, i, rs, rd)
          | A.Div (rd)        => t
          | A.Movr(rs, rd)    => ckMovr (inf, debuginfo, tctx, env, rs, rd)
          | A.Movz(i, rd, tp) => ckMovz (inf, debuginfo, tctx, env, tp, i, rd)
          | A.Movld(i, rs, rd)=> ckMovld (inf, debuginfo, tctx, env, i, rs, rd)
          | A.Movst(rs, i, rd)=> ckMovst (inf, debuginfo, tctx, env, rs, i, rd)
          | A.Xchg(rs, rd)    => ckXchg (inf, debuginfo, tctx, env, rs, rd)
          | A.Leab(i, rs, rd) => t
          | A.Leal(l, rd)     => t
          | A.Cmpr(rs, rd)    => fail ("must be followed by JCC")
          | A.Cmpz(z, rd)     => fail ("must be followed by JCC")
          | A.Pop(rd)         => ckPop (inf, debuginfo, tctx, env, rd)
          | A.Push(rs)        => ckPush (inf, debuginfo, tctx, env, rs)
          | A.Leave           => 
            let val (tctx1, env1) = ckMovr (inf, debuginfo, tctx, env, A.Ebp, A.Esp)
            in ckPop (inf, debuginfo, tctx1, env1, A.Ebp)
            end
          | A.Free(rs)        => ckFree (inf, debuginfo, tctx, env, rs)
          | A.Section(sec)    => t
          | A.Label(str,opta) => t
          | A.Directive(str)  => t
          | A.ExtrA(assert)   => t
          | _                 => t
    end
    
(*cmpr rs rd*)                                
(*@ 
  @
 *)
fun ckCmpr (inf, debuginfo, tctx, env, cblks, rs, rd, instr) =
    let val (pprop, PiP, PiSet, NSet, DSet, USet) = env
        val (asmenv, gamma) = tctx
        val tctx1 = (asmenv, gamma, debuginfo, env) 
        val pndu = (PiSet, NSet, DSet, USet)
        val (rsaptr, rdaptr) = (A.Preg(rs),A.Preg(rd))
        val (rsastr, rdastr) = (A.aptr2str(rsaptr),A.aptr2str(rdaptr))
        val (rstp, rdtp) = (getTypeAll (tctx1, rsaptr), getTypeAll (tctx1, rdaptr))
        val _ = debugPrint ("Now checking instruction : \tcmpr\t"^rsastr^", "^rdastr^" \n")
        val _ = debugPrint ("                           "^(A.toString instr)^" \n")
        val _ = outputInfo (tctx, env) (*Output Info*)
        val fail = fn str => setPosAndFail (debuginfo, tctx, env, str)
        val mylabel = getDebugLabel debuginfo
    in case (rstp, rdtp)
        of (A.Int, A.Int) =>
           let val _ = debugPrint ("int int compare..\n")
           in case instr
               of  A.Jg(l, ln) =>
                   let val _ = setResult (mylabel, l, (gamma, pprop, PiP, PiSet, NSet, DSet, USet))
                       val _ = setResult (mylabel, ln, (gamma, pprop, PiP, PiSet, NSet, DSet, USet))
                       val _ = dumpResult "Internal Results:\n"
                   in ()
                   end
                 | A.Je(l, ln) => 
                   let val _ = setResult (mylabel, l, (gamma, pprop, PiP, PiSet, NSet, DSet, USet))
                       val _ = setResult (mylabel, ln, (gamma, pprop, PiP, PiSet, NSet, DSet, USet))
                       val _ = dumpResult "Internal Results:\n"
                   in ()
                   end
                 | A.Jge(l, ln) => 
                   let val _ = setResult (mylabel, l, (gamma, pprop, PiP, PiSet, NSet, DSet, USet))
                       val _ = setResult (mylabel, ln, (gamma, pprop, PiP, PiSet, NSet, DSet, USet))
                       val _ = dumpResult "Internal Results:\n"
                   in ()
                   end
                 | _ => fail (" Jcc instruction expected...")
           end
         | (_ ,_ ) => fail ("non-int register compare...not allowed")
    end

(*cmpz z rd*)                                
(*@ 
  @
 *)
and ckCmpz (inf, debuginfo, tctx, env, cblks, z, rd, instr) =
    let val (pprop, PiP, PiSet, NSet, DSet, USet) = env
        val (asmenv, gamma) = tctx
        val tctx1 = (asmenv, gamma, debuginfo, env) 
        val pndu = (PiSet, NSet, DSet, USet)
        val rdaptr = A.Preg(rd)
        val rdastr = A.aptr2str(rdaptr)
        val rdtp   = getTypeAll (tctx1, rdaptr)
        val _ = debugPrint ("Now checking instruction : \tcmpz\t"^(Int.toString(z))^", "^rdastr^" \n")
        val _ = debugPrint ("                           "^(A.toString instr)^" \n")
        val _ = outputInfo (tctx, env) (*Output Info*)
        val fail = fn str => setPosAndFail (debuginfo, tctx, env, str)
        val t = ()
        val (envl, envln) = 
            case rdtp
             of A.Int => (env, env)
              | A.Ptr(_) => 
                if z = 0
                then (adjustEnvU2N (rdaptr, env), adjustEnvU2Pi (rdaptr, env))
                else fail ("non-zero integer compare with pointer...not allowed")
              | _ => fail ("non-int nor ptr compare...not allowed")
        val (ppropl, PiPl, PiSetl, NSetl, DSetl, USetl) = envl
        val (ppropln, PiPln, PiSetln, NSetln, DSetln, USetln) = envln
        val mylabel = getDebugLabel debuginfo
    in  case instr
        of  A.Jg(l, ln) => 
            let val _ = setResult (mylabel, l, (gamma, ppropl, PiPl, PiSetl, NSetl, DSetl, USetl))
                val _ = setResult (mylabel, ln, (gamma, ppropln, PiPln, PiSetln, NSetln, DSetln, USetln))
                val _ = dumpResult "Internal Results:\n"
            in ()
            end
          | A.Je(l, ln) => 
            let val _ = setResult (mylabel, l, (gamma, ppropl, PiPl, PiSetl, NSetl, DSetl, USetl))
                val _ = setResult (mylabel, ln, (gamma, ppropln, PiPln, PiSetln, NSetln, DSetln, USetln))
                val _ = dumpResult "Internal Results:\n"
            in ()
            end
          | A.Jge(l, ln) =>
            let val _ = setResult (mylabel, l, (gamma, ppropl, PiPl, PiSetl, NSetl, DSetl, USetl))
                val _ = setResult (mylabel, ln, (gamma, ppropln, PiPln, PiSetln, NSetln, DSetln, USetln))
                val _ = dumpResult "Internal Results:\n"
            in ()
            end
          | _ => fail (" Jcc instruction expected...")
    end
(*Jmp l*)
and ckJmp (inf, debuginfo, tctx, env, cblks, l) = 
    let val (pprop, PiP, PiSet, NSet, DSet, USet) = env
        val (asmenv, gamma) = tctx
        val _ = outputInfo (tctx, env) (*Output Info*) 
        val fail = fn (str, env) => setPosAndFail (debuginfo, tctx, env, str)
        val mylabel = getDebugLabel debuginfo
        val (pprop, PiP, PiSet, NSet, DSet, USet) = env
    in case (getMyCblkAtLabel (cblks, l))
        of NONE => fail (l^" is not a good label... bug...\n", env)
         | SOME cblk => 
           let val _ = setResult (mylabel, l, (gamma, pprop, PiP, PiSet, NSet, DSet, USet))
               val _ = dumpResult "Internal Results:\n"
               val cblk = getMyCblkAtLabel (cblks, l)
           in if isMyCbCheckedInCbs (cblks, l)
              then case cblk
                    of NONE => debugPrint ("***error...\n\n")
                     | SOME cb =>
                       let val (ownenvl, ownenvr) = createEnv ("Try to creating code block env form passert...\n", cb)
                           val (opprop, oPip, oPiSet, oNSet, oDSet, oUSet) = ownenvl
                           val (opprop1, oPip1, oPiSet1, oNSet1, oDSet1, oUSet1) = ownenvr
                       in if isMyCbCycleEntryInCbs (cblks, l) andalso not (isMyCbEntryInCbs(cblks, l))
                          then let val _ = debugPrint ("@cycle entry...\n")
                               in case ownenvr
                                   of (A.Ptrue, A.Ptrue, emp_pi, emp_n, emp_d, emp_u)=>
                                      if checkSinglePNDUImply (env, ownenvl)
                                      then ()
                                      else fail ("Jmp S : Cycle entry wrong imply relationship of Pi N D U!", ownenvl)
                                    | _ =>
                                     if checkSinglePNDUImply (env, ownenvr)
                                     then ()
                                     else fail ("Jmp OR : Cycle entry wrong imply relationship of Pi N D U!", ownenvl)
                               end 
                          else () 
                       end
              else ()
           end
    end

(*Ret*)
and ckRet (inf, debuginfo, tctx, env, cblks) =
    let val _ = debugPrint ("Now checking instruction : \tret \n")
        val _ = outputInfo (tctx, env) (*Output Info*) 
        val newenv = adjustEnv (env, (A.Preg(A.Esp)),4)
        val _ = debugPrint ("adjust esp due to return address pop... \n")
        val _ = outputInfo (tctx, newenv) (*Output Info*) 
        val fail = fn str => setPosAndFail (debuginfo, tctx, env, str)
    in  ()
    end

(*malloc i l #ty*)
and ckMalloc (inf, debuginfo, tctx, env, cblks, i, l ,ty) =
    let val _ = debugPrint ("Now checking instruction : \tmalloc\t"^(Int.toString i)^", "^l^"\n"^(A.etype2str ty))
        val (pprop, PiP, PiSet, NSet, DSet, USet) = env
        val pndu = (PiSet, NSet, DSet, USet)
        val (asmenv, gamma) = tctx
        val tctx1 = (asmenv, gamma, debuginfo, env) 
        val eax = A.Preg(A.Eax)
        val eaxtp = getTypeAll (tctx1, eax)
        val newgamma = setTypeGamma (gamma, A.Preg(A.Eax), A.Ptr(ty))
        val mylabel = getDebugLabel debuginfo
        val _ = outputInfo (tctx, env) (*Output Info*) 
        val fail = fn str => setPosAndFail (debuginfo, tctx, env, str)
    in case eaxtp
        of A.Int =>
           let val _ = debugPrint ("@Eax is int type\n")
               val newPiSet = addSingletonPi (eax, PiSet)
               val _ = setResult (mylabel, l, (newgamma, pprop, PiP, newPiSet, NSet, DSet, USet))
               val _ = dumpResult "Internal Results:\n"
           in ()
           end
         | A.Ptr(_) =>
           let val _ = debugPrint ("@Eax is ptr type\n")
               val (p, n, d, u) = 
                   case getPtrSort (eax, pndu)
                    of P =>
                       let val _ = debugPrint ("@@ eax in pi set\n")
                       in if not_leaking(eax, PiSet)
                          then let val _ = debugPrint ("@@Not leaking...\n") 
                                   val (_, _ , p, n, d, u) = adjustEnvAliasSubst (env, eax)
                                   val p2 = deletePtrPi (eax, p)
                                   val newpi = addSingletonPi (eax, p2)
                               in (newpi, n, d, u)
                               end
                          else fail ("Error: memory leaking detected (caused by malloc)!")
                       end
                     | N =>
                       let val _ = debugPrint ("@@ eax in N set\n")
                           val newn = deletePtrN (eax, NSet)
                           val newpi = addSingletonPi (eax, PiSet)
                       in (newpi, newn, DSet, USet)
                       end
                     | D =>
                       let val _ = debugPrint ("@@ eax in D set\n")
                           val newd = deletePtrD (eax, DSet)
                           val newpi = addSingletonPi (eax, PiSet)
                       in (newpi, NSet, DSet, USet)
                       end
                     | U =>
                       let val _ = debugPrint ("@@ eax in pi set\n")
                           val newu = deletePtrU (eax, USet)
                           val newpi = addSingletonPi (eax, PiSet)
                       in (newpi, NSet, DSet, newu)
                       end
               val _ = setResult (mylabel, l, (newgamma, pprop, PiP, p, n, d, u))
               val _ = dumpResult "Internal Results:\n"
           in ()
           end
         | _ => fail "Eax has wrong type...\n"
    end

(*call f, l*)
and ckCall (inf, debuginfo, tctx, env, cblks, f, l) =
    let val _ = debugPrint ("Now checking instruction : \tcall\t"^f^", "^l^"\n")
        val (pprop, PiP, PiSet, NSet, DSet, USet) = env
        val pndu = (PiSet, NSet, DSet, USet)
        val (asmenv, gamma) = tctx
        val eax = A.Preg(A.Eax)
        val tctx1 = (asmenv, gamma, debuginfo, env)
        val eaxtp = getTypeAll(tctx1, eax)
        val mylabel = getDebugLabel debuginfo
        val _ = outputInfo (tctx, env) (*Output Info*) 
        val fail = fn str => setPosAndFail (debuginfo, tctx, env, str)
        fun ckParameter (ctx, fplist) = 
            case fplist
             of [] => true
              | (aptr, tp)::xs=>
                if getTypeAll (ctx, aptr) = tp
                then ckParameter (ctx, xs)
                else false
    in if f = "print"
       then let val _ = debugPrint "print\n"
                val _ = setResult (mylabel, l, (gamma, pprop, PiP, PiSet, NSet, DSet, USet))
                val _ = dumpResult "Internal Results:\n"
            in ()
            end
       else let val frettp = getFnRetType(f, inf)
                val fplist = getFnParameters f
            in if ckParameter(tctx1, fplist)
               then let val _ = debugPrint "@Function Parameter(s) is/are OK...\n"
                    in case (eaxtp, frettp)
                        of (A.Int, A.Int) =>
                           let val _ = setResult (mylabel, l, (gamma, pprop, PiP, PiSet, NSet, DSet, USet))
                               val _ = dumpResult "Internal Results:\n"
                           in ()
                           end
                         | (A.Int, A.Ptr(t1)) =>
                           let val newgamma = setTypeGamma (gamma, eax, frettp)
                               val newpi = addSingletonPi (eax, PiSet)
                               val _ = setResult (mylabel, l, (newgamma, pprop, PiP, newpi, NSet, DSet, USet))
                               val _ = dumpResult "Internal Results:\n"
                           in ()
                           end                
                         | (A.Ptr(t1), A.Int) =>
                           (case getPtrSort (eax, pndu)
                             of P =>
                                let val _ = debugPrint ("@@ eax in pi set\n")
                                in if not_leaking(eax, PiSet)
                                   then let val _ = debugPrint ("@@Not leaking...\n") 
                                            val (_, _ , p, n, d, u) = adjustEnvAliasSubst (env, eax)
                                            val p2 = deletePtrPi (eax, p)
                                            val newgamma = setTypeGamma (gamma, eax, frettp)
                                            val _ = setResult (mylabel, l, (newgamma, pprop, PiP, p2, n, d, u))
                                            val _ = dumpResult "Internal Results:\n"
                                        in ()
                                        end
                                   else fail ("Error: memory leaking detected (caused by call)!")
                                end
                              | N =>
                                let val _ = debugPrint ("@@ eax in N set\n")
                                    val newn = deletePtrN (eax, NSet)
                                    val newgamma = setTypeGamma (gamma, eax, frettp)
                                    val _ = setResult (mylabel, l, (newgamma, pprop, PiP, PiSet, newn, DSet, USet))
                                    val _ = dumpResult "Internal Results:\n"
                                in ()
                                end
                              | D =>
                                let val _ = debugPrint ("@@ eax in D set\n")
                                    val newd = deletePtrD (eax, DSet)
                                    val newgamma = setTypeGamma (gamma, eax, frettp)
                                    val _ = setResult (mylabel, l, (newgamma, pprop, PiP, PiSet, NSet, newd, USet))
                                    val _ = dumpResult "Internal Results:\n"
                                in ()
                                end
                              | U =>
                                let val _ = debugPrint ("@@ eax in pi set\n")
                                    val newu = deletePtrU (eax, USet)
                                    val newgamma = setTypeGamma (gamma, eax, frettp)
                                    val _ = setResult (mylabel, l, (newgamma, pprop, PiP, PiSet, NSet, DSet, newu))
                                    val _ = dumpResult "Internal Results:\n"
                                in ()
                                end)
                         | (A.Ptr(t1), A.Ptr(t2)) =>
                           (case getPtrSort (eax, pndu)
                             of P =>
                                let val _ = debugPrint ("@@ eax in pi set\n")
                                in if not_leaking(eax, PiSet)
                                   then let val _ = debugPrint ("@@Not leaking...\n") 
                                            val (_, _ , p, n, d, u) = adjustEnvAliasSubst (env, eax)
                                            val p2 = deletePtrPi (eax, p)
                                            val p3 = addSingletonPi(eax, p2)
                                            val newgamma = setTypeGamma (gamma, eax, frettp)
                                            val _ = setResult (mylabel, l, (newgamma, pprop, PiP, p3, n, d, u))
                                            val _ = dumpResult "Internal Results:\n"
                                        in ()
                                        end
                                   else fail ("Error: memory leaking detected (caused by call)!")
                                end
                              | N =>
                                let val _ = debugPrint ("@@ eax in N set\n")
                                    val newn = deletePtrN (eax, NSet)
                                    val newp = addSingletonPi(eax, PiSet)
                                    val newgamma = setTypeGamma (gamma, eax, frettp)
                                    val _ = setResult (mylabel, l, (newgamma, pprop, PiP, newp, newn, DSet, USet))
                                    val _ = dumpResult "Internal Results:\n"
                                in ()
                                end
                              | D =>
                                let val _ = debugPrint ("@@ eax in D set\n")
                                    val newd = deletePtrD (eax, DSet)
                                    val newp = addSingletonPi(eax, PiSet)
                                    val newgamma = setTypeGamma (gamma, eax, frettp)
                                    val _ = setResult (mylabel, l, (newgamma, pprop, PiP, newp, NSet, newd, USet))
                                    val _ = dumpResult "Internal Results:\n"
                                in ()
                                end
                              | U =>
                                let val _ = debugPrint ("@@ eax in pi set\n")
                                    val newu = deletePtrU (eax, USet)
                                    val newp = addSingletonPi(eax, PiSet)
                                    val newgamma = setTypeGamma (gamma, eax, frettp)
                                    val _ = setResult (mylabel, l, (newgamma, pprop, PiP, newp, NSet, DSet, newu))
                                    val _ = dumpResult "Internal Results:\n"
                                in ()
                                end)
                         | (A.Int, A.Wild) =>
                           let val _ = setResult (mylabel, l, (gamma, pprop, PiP, PiSet, NSet, DSet, USet))
                               val _ = dumpResult "Internal Results:\n"
                           in ()
                           end
                         | (A.Int, _ ) =>
                           fail "Unsuported Function Return Type!"
                         | (A.Ptr(_), A.Wild) =>
                           let val _ = setResult (mylabel, l, (gamma, pprop, PiP, PiSet, NSet, DSet, USet))
                               val _ = dumpResult "Internal Results:\n"
                           in ()
                           end
                         |(A.Ptr(_), _)=>
                          fail "Unsuported Function Return Type!"
                         | _ => fail "Corrupted Eax Type!"
                    end
               else fail "Function Call : Parameter(s) type error!"
            end
    end
        
(*check last instruction*)
and ckLastInstr (inf, debuginfo, tctx, env, cblks, instr) =
    let val _ = debugPrint ("Now checking Last instruction : "^(A.toString instr)^" \n")
        val ndinfo = setDebugInstr (debuginfo, instr)
        val t = ()
    in  case instr
         of A.Jmp(l)           => ckJmp (inf, ndinfo, tctx, env, cblks, l)
          | A.Malloc(i, l, tp) => ckMalloc (inf, ndinfo, tctx, env, cblks, i, l, tp)
          | A.Call(f,l)        => ckCall (inf, ndinfo, tctx, env, cblks, f, l)
          | A.Ret(l)           => ckRet (inf, ndinfo, tctx, env, cblks)
          | _                  => t
    end

(*instruction list*)
and ckInstrs (inf, debuginfo, tctx, env, cblks, instrs) =
    case instrs 
     of [] => ()
      | instr::[] => ckLastInstr (inf, debuginfo, tctx, env, cblks, instr)
      | A.Cmpz(z, rd)::instr::[] => 
        let val ndinfo = setDebugInstr (debuginfo, A.Cmpz(z, rd))
        in ckCmpz(inf, ndinfo, tctx, env, cblks, z, rd, instr)
        end
      | A.Cmpr(rs,rd)::instr::[] => 
        let val ndinfo = setDebugInstr (debuginfo, A.Cmpr(rs, rd))
        in ckCmpr(inf, ndinfo, tctx, env, cblks, rs, rd, instr)
        end
      | instr::instrss => let val (newTctx, newEnv) = ckInstr (inf, debuginfo, tctx, env, cblks, instr)
                          in ckInstrs (inf, debuginfo, newTctx, newEnv, cblks, instrss)
                          end       
                          
(*Code Block*)
and ckCblk (inf, debuginfo, tctx, env, cblks, cblk) =
    let val label = (cblkLabel cblk)
        val (asmenv, gamma) = tctx
        val _ = debugPrint ("Basic code block label : "^label^"\n")
        val _ = debugPrint ("This block has "^(cblkCnum cblk)^" instructions\n")
        val (ownenvl, ownenvr) = createEnv ("Try to creating code block env form passert...\n", cblk)
        val (pprop, PiP, PiSet, NSet, DSet, USet) = env
        val (opprop, oPip, oPiSet, oNSet, oDSet, oUSet) = ownenvl
        val (opprop1, oPip1, oPiSet1, oNSet1, oDSet1, oUSet1) = ownenvr
        val _ = outputInfo (tctx, env) (*Output Info*) 
        val newDebuginfo = setDebugLabel (debuginfo, label) 
        val fail = fn (str, env) => setPosAndFail (newDebuginfo, tctx, env, str)
    in if isMyCbCheckedInCbs (cblks, label) 
       then cblks (*this block is checked then do nothing*)
       else let val cblks1 = setMyCbChecked (cblks, label)                
            in if (opprop = A.Ptrue) (*no assertion born at this block*)
               then if (pprop = A.Ptrue) (*no assertion from father block*)
                    then (*cblks1*) (*do nothing to None-Ptr-Program*)
                        let val _ = ckInstrs (inf, newDebuginfo, tctx, env, cblks1, (cblkCode cblk))
                        in cblks1
                        end
                    else if isPiNDUCorrect (PiSet, NSet, DSet, USet) 
                         then let val _ = ckInstrs (inf, newDebuginfo, tctx, env, cblks1, (cblkCode cblk))
                              in cblks1
                              end
                         else fail ("Env Pi N D U is not correct ..", env)
               else if isMyCbCycleEntryInCbs (cblks, label) andalso not (isMyCbEntryInCbs(cblks, label))
                    then let val _ = debugPrint ("This is a cycle entry...\n")
                             val _ = debugPrint ("@Propl : "^A.pprop2str(opprop)^"\n")
                             val _ = debugPrint ("@Propr : "^A.pprop2str(opprop1)^"\n")
                         in case ownenvr
                             of (A.Ptrue, A.Ptrue, emp_pi, emp_n, emp_d, emp_u)=>
                                if checkSinglePNDUImply (env, ownenvl)
                                then let val newU = PiSet.union (USet, oUSet)
                                         val newenv = (opprop, oPip, PiSet, NSet, DSet, newU)
                                         val newgamma = changeGammaForUSet (tctx, oPip)
                                         val _ = ckInstrs(inf, newDebuginfo, (asmenv, newgamma), newenv, cblks1, (cblkCode cblk))
                                     in cblks1
                                     end
                                else fail ("Cycle enty wrong imply relationship of Pi N D U!", ownenvl)
                              | _ =>
                                if (checkSinglePNDUImply (env, ownenvl))
                                then let val newU = PiSet.union (USet, oUSet)
                                         val newenv = (opprop, oPip, PiSet, NSet, DSet, newU)
                                         val newgamma = changeGammaForUSet (tctx, oPip)
                                         val _ = ckInstrs(inf, newDebuginfo, (asmenv, newgamma), newenv, cblks1, (cblkCode cblk))
                                     in cblks1
                                     end
                                else fail ("Cycle enty wrong imply relationship of Pi N D U!", ownenvl)
                         end 
                    else if isPiNDUCorrect (oPiSet, oNSet, oDSet, oUSet)
                         then let val _ = debugPrint ("Using own env ...\n")
                                  val _ = ckInstrs(inf, newDebuginfo, tctx, ownenvl, cblks1, (cblkCode cblk))
                              in cblks1
                              end
                         else fail ("Own Env Pi N D U is not correct ..", ownenvl)            
            end
    end

(*union two results caused by if-then-else*)
and unionResults(debuginfo, genv1, genv2) = 
    let val (g1, pp1, pip1, p1, n1, d1, u1) = genv1
        val (g2, pp2, pip2, p2, n2, d2, u2) = genv2
        val fail = fn str => 
                      (print  ("Asmprover found error in: \n"^
                               (getDebugInfoStr (setDebugPos(debuginfo,str)))^"\n") 
                     ; raise AsmProverFail)
        fun findCommonN (n1, n2) =
            let val (l1, l2) = (toList n1, toList n2)
                fun findCommonList (l, n) = 
                    case l
                     of [] => [] 
                      |x :: xs => 
                       if isPtrInN (x, n)
                       then x::(findCommonList(xs, n))
                       else findCommonList(xs, n)
                val clist = findCommonList (l1, n2)
            in toSet clist
            end  
        fun findSetDiff (set1, set2) =
            let val (l1, l2) = (toList set1, toList set2)
                fun findDiffList (l, set) =
                    case l
                     of [] => []
                      | x::xs =>
                        if isPtrInN (x, set)
                        then findDiffList(xs, set)
                        else x::(findDiffList(xs, set))
                val dlist = findDiffList (l1, set2)
            in toSet dlist
            end

        fun isSetMemberInPi(n1, p2) = 
            if isEmptyN n1 
            then true
            else let val nlist = toList n1
                     val aptr = List.hd nlist
                     val piset = (set2elem (getPtrSet (aptr, p2)))
                     fun cklist (l, set) =
                         case l 
                          of [] => true
                           | x::xs =>
                             if isPtrInN (x, piset)
                             then cklist (xs, set)
                             else false               
                 in if cklist (nlist, piset)
                    then true
                    else false
                 end

        fun adjustN (n1, p1) =
            let val l1 = toList n1
                fun change l =
                    case l
                     of [] => n1
                      | x::xs =>
                        (case x
                          of A.Pstk(off, reg) =>
                             if isPtrInPi (A.Preg(reg), p1)
                             then let val alias = getAnotherPtrSameSetPi(A.Preg(reg), p1)
                                  in (case alias
                                       of A.Preg _ => change xs
                                        |_ => adjustN (adjustNDBase(A.Preg(reg), alias, n1), p1))
                                  end
                             else change xs
                           | _ => change xs)
            in (change l1)
            end
        fun getPU (p1, p2, n1, u1) =
            if not (isEmptyN n1)
            then let val newn1 = deleteNDBaseReg n1 (*adjustN (n1, p1)*)
                     val newp  = if isEmptyN newn1 then p2 else deletePtrSetPi (List.hd (toList newn1), p2)
                     val newp2 = deleteRegPtrPi (newp)
                     val newu1 = if isEmptyN newn1 then u1 else PiSet.add(u1, newn1)
                 in if isSetMemberInPi (newn1, p2)
                    then (newp2, newu1)
                    else (deleteRegPtrPi(p2), newu1)
                 end
            else (deleteRegPtrPi(p2), u1)
        
        fun getUSet (u1, u2) = 
            let val _ = printSetset (debugPrint, u1)
                val u11 = deleteUBaseReg u1
                val _ = printSetset (debugPrint, u11)
                val u22 = deleteUBaseReg u2
            in PiSet.union(u11, u22)
            end
            
        fun getPNU (p1,p2, nc, n1d, n2d, u1, u2) =
            let val n = nc
                val (newp2, newu1) = getPU (p1,p2,n1d,u1)
                val (newp1, newu2) = getPU (p2,p1,n2d,u2)  
                val uset = getUSet (newu1, newu2)
            in (PiSet.union(newp1, newp2), nc, uset)
            end
    in if not (isEqD (d1, d2))
       then fail "two branches have different D Set"
       else let val _ = debugPrint "DSets are equal\n"
                val commonn = findCommonN (n1, n2)
                val _ = printSet (debugPrint, commonn)
                val n1d = findSetDiff(n1, commonn)
                val n2d = findSetDiff(n2, commonn)
                val p1 = deleteUBaseReg p1
                val p2 = deleteUBaseReg p2
                val (newp, newn, newu) = getPNU (p1,p2, commonn, n1d, n2d, u1, u2)
                val g2 = removeGammaReg g1             
            in (g2, pp1, pip1, newp, newn , d2, newu)
            end
    end

(*Find next ready code block to check and check it*)
and findNextCblkAndCheck (inf, debuginfo, asmenv, cblks, subclbks) =
    let val _ = debugPrint ("\nTry to find next label of block to check...\n")
    in case subclbks
        of [] => 
           let val _ = debugPrint ("No Basic Block in this function has not been checked.\n")
           in ()
           end
         | cblk::cblkss =>
           let val label = getMyCbLab cblk
           in if isMyCbCheckedInCbs (cblks, label)
              then let val _ = debugPrint ("Basic Block "^label^" has been checked\n")
                   in findNextCblkAndCheck (inf, debuginfo, asmenv, cblks, cblkss)
                   end
              else let val _ = debugPrint ("Basic Block "^label^" has not been checked...\n")
                       val fs = getFatherOf (cblks, label)
                       val n = List.length (fs)
                       val _ = debugPrint ("There is/are "^Int.toString(n)^" blocks that will jump/branch to it\n")
                    in case n
                        of 0 => findNextCblkAndCheck (inf, debuginfo, asmenv, cblks, cblkss)
                         | 1 =>
                           if isMyCbCheckedInCbs (cblks, List.hd (fs))
                           then let val _ = debugPrint ("Father Basic Block "^List.hd(fs)^" has been checked\n") 
                                    val (l1, l2) = (List.hd (fs), label)
                                    val nextcblk = getMyCblkAtLabel (cblks, l2)
                                in case nextcblk
                                    of NONE => debugPrint ("***error...\n\n")
                                     | SOME cb =>
                                       if isInResult (l1, l2) 
                                       then let val (g, pp, pip, p, n, d, u) = getResult (l1, l2)
                                                val  cblksm = ckCblk (inf, debuginfo, (asmenv, g), (pp, pip, p, n, d, u), cblks, cb)
                                            in findNextCblkAndCheck (inf, debuginfo, asmenv, cblksm, cblkss)
                                            end
                                       else findNextCblkAndCheck (inf, debuginfo, asmenv, cblks, cblkss)
                                end
                           else let val _ = debugPrint ("Father Basic Block "^List.hd(fs)^" has not been checked\n") 
                                in findNextCblkAndCheck (inf, debuginfo, asmenv, cblks, cblkss)
                                end
                         | 2 =>
                           if isMyCbCycleEntryInCbs (cblks, label)
                           then let val _ = debugPrint (label^" is a Cycle entry\n")
                                    val label1 = if isMyCbCheckedInCbs (cblks, List.hd fs)
                                                 then List.hd fs
                                                 else if isMyCbCheckedInCbs (cblks, List.hd (List.tl fs))
                                                      then  List.hd (List.tl fs)
                                                      else ""
                                in if label1 = "" 
                                   then findNextCblkAndCheck (inf, debuginfo, asmenv, cblks, cblkss)
                                   else let val (l1, l2) = (label1, label)
                                            val nextcblk = getMyCblkAtLabel (cblks, l2)
                                        in case nextcblk
                                            of NONE => debugPrint ("***error...\n\n")
                                             | SOME cb =>
                                               if isInResult (l1, l2) 
                                               then let val (g, pp, pip, p, n, d, u) = getResult (l1, l2)
                                                        val cblksm = 
                                                            ckCblk (inf, debuginfo, (asmenv, g), (pp, pip, p, n, d, u), cblks, cb)
                                                    in findNextCblkAndCheck (inf, debuginfo, asmenv, cblksm, cblkss)
                                                    end
                                               else findNextCblkAndCheck (inf, debuginfo, asmenv, cblks, cblkss)
                                        end
                                end
                           else let val _ = debugPrint (label^" is not a Cycle entry\n")
                                in if isMyCbCheckedInCbs (cblks, List.hd fs) andalso isMyCbCheckedInCbs (cblks, List.hd (List.tl fs))
                                   then let val _ = debugPrint "Two father blocks have been checked!\n"
                                            val genv1 = getResult (List.hd fs, label)
                                            val genv2 = getResult (List.hd (List.tl fs), label)
                                            val (g, pp, pip, p, n, d, u) = unionResults(debuginfo, genv1, genv2)
                                            val cblk = getMyCblkAtLabel (cblks, label)
                                        in case cblk
                                            of NONE => (print ("The basic code block of Label: "^label^" is empty...") 
                                                      ; raise AsmProverFail)
                                             | SOME cb => 
                                               let val cblksm = ckCblk (inf, debuginfo, (asmenv, g), (pp, pip, p, n, d, u), cblks, cb)
                                               in findNextCblkAndCheck (inf, debuginfo, asmenv, cblksm, cblkss)
                                               end
                                        end
                                   else findNextCblkAndCheck (inf, debuginfo, asmenv, cblks, cblkss)
                                end
                         | _ => debugPrint "not supported yet\n"
                   end    
           end           
    end

(*Code Blocks*)
fun ckCblks (inf, debuginfo, tctx, cblks) = 
    let val initenv = initEnv ("Initiating initial enviroment...\n")
        val (asmenv, gamma) = tctx
        val _ = case cblks
                 of [] => ()
                  | cblk :: cblks1 => 
                    let val cblksm = ckCblk (inf, debuginfo, tctx, initenv, cblks, cblk)
                    in findNextCblkAndCheck (inf, debuginfo, asmenv, cblksm, cblks1)
                    end
    in ()
    end
    
(*Function*)
fun ckPrf (inf, prf) = 
    let val _ = (debugPrint ("Function "^(fname prf)^"\n"))
        val _ = (debugPrint ("Pre-condition: "); outputPprop (A.getPre prf, not (debugFlag())))
        val _ = (debugPrint ("Post-condition: "); outputPprop (A.getPost prf, not (debugFlag())))
        val _ = (debugPrint ("Function "^(fname prf)^" has "^(fcblksNum prf)^" basic blocks\n\n"))
        val _ = postcondition := (A.getPost prf)
        val mycblks = cbs2mycbs (fcblks prf)
        val _ = cblks := mycblks
        val asmenv  = A.getAsmEnv prf
        val gamma   = emp_gamma 
        val tctx    = (asmenv, gamma)
        val debuginfo = setDebugFname (fname prf)
        val _ = initResult "xxx"
    in  ckCblks (inf, debuginfo, tctx, mycblks)
    end

(*Program - Functions*)
fun top (prflist, inf) =
    let val _ = debugPrint "ASMProver checking...\n\n"
        val _ = if List.null prflist 
                then debugPrint ("Empty prflist!\n") 
                else debugPrint ("Function by Function checking start...\n")
        val _ = plist := prflist
    in  (List.app (fn prf => ckPrf (inf,prf)) prflist 
       ;(debugPrint ("Function by Function checking end...\nASMProver checking finished successfully...\n\n")))
    end

end
